diff -ruN coq-8.4pl1/add_smartcatch.ml coq-8.4pl1-withexn/add_smartcatch.ml
--- coq-8.4pl1/add_smartcatch.ml	1970-01-01 01:00:00.000000000 +0100
+++ coq-8.4pl1-withexn/add_smartcatch.ml	2013-03-07 16:08:19.918361247 +0100
@@ -0,0 +1,41 @@
+open Camlp4;
+
+module Id = struct
+  value name    = "JHwith";
+  value version = "0.1";
+end;
+
+module Make (AstFilters : Camlp4.Sig.AstFilters) = struct
+  open AstFilters;
+  open Ast;
+
+  value add_debug_expr _loc patvar e =
+    <:expr<
+        (* put your stuff here *)
+        let _ = ExceptionHandling.register $lid:patvar$ in
+        $e$
+    >>;
+
+  value rec map_handler =
+    let patvar = "__exn" in
+    fun
+    [ <:match_case@_loc< $m1$ | $m2$ >> ->
+        <:match_case< $map_handler m1$ | $map_handler m2$ >>
+    | <:match_case@_loc< $p$ when $w$ -> $e$ >> ->
+        <:match_case@_loc<
+          ($p$ as $lid:patvar$) when $w$ -> $add_debug_expr _loc patvar e$ >>
+    | m -> m ];
+
+  value filter = object
+    inherit Ast.map as super;
+    method expr = fun
+    [ <:expr@_loc< try $e$ with [ $h$ ] >> ->
+      <:expr< try $e$ with [ $map_handler h$ ] >>
+    | x -> super#expr x ];
+  end;
+
+  register_str_item_filter filter#str_item;
+
+end;
+
+let module M = Camlp4.Register.AstFilter Id Make in ();
diff -ruN coq-8.4pl1/checker/check.mllib coq-8.4pl1-withexn/checker/check.mllib
--- coq-8.4pl1/checker/check.mllib	2010-01-08 18:03:54.000000000 +0100
+++ coq-8.4pl1-withexn/checker/check.mllib	2013-02-28 16:19:20.980323654 +0100
@@ -1,4 +1,5 @@
 Coq_config
+ExceptionHandling
 Pp_control
 Pp
 Compat
diff -ruN coq-8.4pl1/dev/printers.mllib coq-8.4pl1-withexn/dev/printers.mllib
--- coq-8.4pl1/dev/printers.mllib	2012-01-21 00:52:15.000000000 +0100
+++ coq-8.4pl1-withexn/dev/printers.mllib	2013-02-28 16:19:16.410417576 +0100
@@ -1,5 +1,6 @@
 Coq_config
 
+ExceptionHandling
 Pp_control
 Pp
 Compat
diff -ruN coq-8.4pl1/lib/errors.ml coq-8.4pl1-withexn/lib/errors.ml
--- coq-8.4pl1/lib/errors.ml	2011-05-17 19:02:59.000000000 +0200
+++ coq-8.4pl1-withexn/lib/errors.ml	2013-03-07 11:59:21.714419279 +0100
@@ -37,7 +37,9 @@
 let where s =
   if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
 
-let raw_anomaly e = match e with
+let raw_anomaly e = 
+  ExceptionHandling.print_backtraces_of stdout e;
+  match e with
   | Util.Anomaly (s,pps) -> where s ++ pps ++ str "."
   | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
   | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
diff -ruN coq-8.4pl1/lib/exceptionHandling.mli coq-8.4pl1-withexn/lib/exceptionHandling.mli
--- coq-8.4pl1/lib/exceptionHandling.mli	1970-01-01 01:00:00.000000000 +0100
+++ coq-8.4pl1-withexn/lib/exceptionHandling.mli	2013-02-28 17:43:26.787045627 +0100
@@ -0,0 +1,5 @@
+(* to be called just after with, to record backtraces *)
+val register : exn -> unit
+
+(* print them on the given channel *)
+val print_backtraces_of : out_channel -> exn -> unit
diff -ruN coq-8.4pl1/lib/lib.mllib coq-8.4pl1-withexn/lib/lib.mllib
--- coq-8.4pl1/lib/lib.mllib	2011-11-24 14:09:24.000000000 +0100
+++ coq-8.4pl1-withexn/lib/lib.mllib	2013-02-28 16:19:32.222092584 +0100
@@ -1,3 +1,4 @@
+ExceptionHandling
 Xml_lexer
 Xml_parser
 Xml_utils
diff -ruN coq-8.4pl1/Makefile.build coq-8.4pl1-withexn/Makefile.build
--- coq-8.4pl1/Makefile.build	2012-10-29 15:46:37.000000000 +0100
+++ coq-8.4pl1-withexn/Makefile.build	2013-02-28 16:19:23.684268079 +0100
@@ -61,7 +61,7 @@
 NO_RECOMPILE_ML4=
 NO_RECOMPILE_LIB=
 NO_RECALC_DEPS=
-READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
+READABLE_ML4=T	# non-empty means .ml of .ml4 will be ascii instead of binary
 VALIDATE=
 COQ_XML=	# is "-xml" when building XML library
 VM=		# is "-no-vm" to not use the vm"
@@ -90,8 +90,8 @@
 
 BAREBYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
 BAREOPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
-BYTEFLAGS=$(MLINCLUDES) $(BAREBYTEFLAGS)
-OPTFLAGS=$(MLINCLUDES) $(BAREOPTFLAGS)
+BYTEFLAGS=-pp 'bash preprocess.sh' $(MLINCLUDES) $(BAREBYTEFLAGS)
+OPTFLAGS=-pp 'bash preprocess.sh' $(MLINCLUDES) $(BAREOPTFLAGS)
 DEPFLAGS= -slash $(LOCALINCLUDES)
 
 define bestocaml
@@ -515,6 +515,7 @@
 # coqdep_boot.
 
 COQDEPBOOTSRC:= \
+  lib/exceptionHandling$(BESTOBJ) \
   tools/coqdep_lexer.mli tools/coqdep_lexer.ml \
   tools/coqdep_common.mli tools/coqdep_common.ml \
   tools/coqdep_boot.ml
@@ -529,19 +530,19 @@
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD))
 
-$(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina)
+$(GALLINA): $(addsuffix $(BESTOBJ), lib/exceptionHandling tools/gallina_lexer tools/gallina)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,)
 
-$(COQMAKEFILE): $(addsuffix $(BESTOBJ),config/coq_config ide/minilib ide/project_file tools/coq_makefile)
+$(COQMAKEFILE): $(addsuffix $(BESTOBJ),config/coq_config lib/exceptionHandling ide/minilib ide/project_file tools/coq_makefile)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,str unix)
 
-$(COQTEX): tools/coq_tex$(BESTOBJ)
+$(COQTEX): lib/exceptionHandling$(BESTOBJ) tools/coq_tex$(BESTOBJ)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,str)
 
-$(COQWC): tools/coqwc$(BESTOBJ)
+$(COQWC): lib/exceptionHandling$(BESTOBJ) tools/coqwc$(BESTOBJ)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,)
 
@@ -552,7 +553,7 @@
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
-$(FAKEIDE): lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BESTOBJ) toplevel/ide_intf$(BESTOBJ) tools/fake_ide$(BESTOBJ)
+$(FAKEIDE): lib/exceptionHandling$(BESTOBJ) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_utils$(BESTOBJ) toplevel/ide_intf$(BESTOBJ) tools/fake_ide$(BESTOBJ)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,unix)
 
@@ -560,9 +561,11 @@
 
 ifeq ($(CAMLP4),camlp4)
 tools/compat5.cmo: tools/compat5.mlp
-	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
+	$(CAMLP4O) -impl $< -o tools/compat5.preprocessed_mlp
+	$(OCAMLC) -c -I $(MYCAMLP4LIB) -impl tools/compat5.preprocessed_mlp
 tools/compat5b.cmo: tools/compat5b.mlp
-	$(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -impl' -impl $<
+	$(CAMLP4O) -impl $< -o tools/compat5b.preprocessed_mlp
+	$(OCAMLC) -c -I $(MYCAMLP4LIB) -impl tools/compat5b.preprocessed_mlp
 else
 tools/compat5.cmo: tools/compat5.ml
 	$(OCAMLC) -c $<
@@ -570,6 +573,20 @@
 	$(OCAMLC) -c $<
 endif
 
+# Special rule deactivating preprocessing for exceptionHandling.ml
+
+lib/exceptionHandling.cmo: lib/exceptionHandling.ml lib/exceptionHandling.cmi
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -pp cat -c $<
+
+lib/exceptionHandling.cmi: lib/exceptionHandling.mli
+	$(SHOW)'OCAMLC    $<'
+	$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -pp cat -c $<
+
+lib/exceptionHandling.cmx: lib/exceptionHandling.ml lib/exceptionHandling.cmi
+	$(SHOW)'OCAMLOPT  $<'
+	$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -pp cat $(HACKMLI) -c $<
+
 ###########################################################################
 # Installation
 ###########################################################################
@@ -747,11 +764,13 @@
 parsing/grammar.cma: | parsing/grammar.mllib.d
 	$(SHOW)'Testing $@'
 	@touch test.ml4
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp '$(CAMLP4O) -I $(CAMLLIB) $^ -impl' -impl test.ml4 -o test-grammar
+	$(HIDE)$(CAMLP4O) $(PR_O) -I $(CAMLLIB) $^ -impl test.ml4 -o test.ml
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -impl test.ml -o test-grammar
 	@rm -f test-grammar test.*
 	$(SHOW)'OCAMLC -a $@'   
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@
 
+
 # toplevel/mltop.ml4 (ifdef Byte)
 
 ## NB: mltop.ml correspond to the byte version (and hence need no special rules)
diff -ruN coq-8.4pl1/Makefile.common coq-8.4pl1-withexn/Makefile.common
--- coq-8.4pl1/Makefile.common	2012-10-29 15:46:40.000000000 +0100
+++ coq-8.4pl1-withexn/Makefile.common	2013-02-28 16:18:28.354404834 +0100
@@ -242,6 +242,7 @@
 # coqmktop, coqc
 
 COQENVCMO:=$(CONFIG) \
+  lib/exceptionHandling.cmo \
   lib/pp_control.cmo lib/pp.cmo  lib/compat.cmo lib/flags.cmo \
   lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/errors.cmo lib/system.cmo \
   lib/envars.cmo
@@ -252,7 +253,8 @@
 
 ## Misc
 
-CSDPCERTCMO:=$(addprefix plugins/micromega/, \
+CSDPCERTCMO:=lib/exceptionHandling.cmo \
+  $(addprefix plugins/micromega/, \
   mutils.cmo 	micromega.cmo \
   sos_types.cmo sos_lib.cmo sos.cmo 	csdpcert.cmo )
 
@@ -260,7 +262,7 @@
 
 COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
 
-COQDOCCMO:=$(CONFIG) $(addprefix tools/coqdoc/, \
+COQDOCCMO:=$(CONFIG) lib/exceptionHandling.cmo $(addprefix tools/coqdoc/, \
   cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo )
 
 ###########################################################################
diff -ruN coq-8.4pl1/parsing/grammar.mllib coq-8.4pl1-withexn/parsing/grammar.mllib
--- coq-8.4pl1/parsing/grammar.mllib	2011-07-29 16:23:55.000000000 +0200
+++ coq-8.4pl1-withexn/parsing/grammar.mllib	2013-02-28 16:19:27.490189851 +0100
@@ -1,5 +1,6 @@
 Coq_config
 
+ExceptionHandling
 Profile
 Pp_control
 Pp
diff -ruN coq-8.4pl1/preprocess.sh coq-8.4pl1-withexn/preprocess.sh
--- coq-8.4pl1/preprocess.sh	1970-01-01 01:00:00.000000000 +0100
+++ coq-8.4pl1-withexn/preprocess.sh	2013-03-07 16:12:31.412342493 +0100
@@ -0,0 +1,13 @@
+#/bin/bash
+
+if [ ! -f add_smartcatch.cmo ];
+then
+    ocamlfind ocamlc -pp camlp4rf -package camlp4 -c add_smartcatch.ml
+fi
+
+if [ ${1: -4} == ".mli" ]
+then
+    exec cat $1
+else
+    exec camlp4o add_smartcatch.cmo -no_quot -impl $1
+fi