Merge tag 'upstream/8.4pl2dfsg' into experimental/master

Upstream version 8.4pl2dfsg

170 files changed, 1205 insertions, 632 deletions

diff --git a/CHANGES b/CHANGES
index fa0cca0c..a696ad71 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,30 @@
+Changes from V8.4pl1 to V8.4pl2
+===============================
+
+Bug fixes
+
+- Solved bugs :
+  #2466 #2629 #2668 #2750 #2839 #2869 #2954 #2955 #2959 #2962 #2966 #2967
+  #2969 #2970 #2975 #2976 #2977 #2978 #2981 #2983 #2995 #3000 #3004 #3008 
+- Partially fixed bugs : #2830 #2949
+- Coqtop should now react more reliably when receiving interrupt signals:
+  all the "try...with" constructs have been protected against undue
+  handling of the Sys.Break exception.
+
+Coqide
+
+- The Windows-specific code handling the interrupt button of Coqide
+  had to be reworked (cf. bug #2869). Now, in Win32 this button does
+  not target a specific coqtop client, but instead sends a Ctrl-C to
+  any process sharing its console with Coqide. To avoid awkward
+  effects, it is recommended to launch Coqide via its icon, its menu,
+  or in a dedicated console window.
+
+Extraction
+
+- The option Extraction AccessOpaque is now set by default,
+  restoring compatibility of older versions of Coq (cf bug #2952).
+
 Changes from V8.4 to V8.4pl1
 ============================
 
@@ -2438,3 +2465,5 @@ New user contributions
 
 - Correctness proof of Stalmarck tautology checker algorithm
   [Stalmarck] (Laurent Théry, Pierre Letouzey, Sophia-Antipolis)
+
+ LocalWords:  recommended
diff --git a/checker/check.ml b/checker/check.ml
index 237eb079..fb0dc12a 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -290,9 +290,9 @@ let intern_from_file (dir, f) =
   let (md,table,digest) =
     try
       let ch = with_magic_number_check raw_intern_library f in
-      let (md:library_disk) = System.marshal_in ch in
-      let digest = System.marshal_in ch in
-      let table = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in
+      let (md:library_disk) = System.marshal_in f ch in
+      let digest = System.marshal_in f ch in
+      let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in
       close_in ch;
       if dir <> md.md_name then
         errorlabstrm "load_physical_library"
diff --git a/checker/checker.ml b/checker/checker.ml
index 945abde4..e5e20b1a 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -371,7 +371,8 @@ let run () =
     compile_files ();
     flush_all()
   with e ->
-    (Pp.ppnl(explain_exn e);
+    (flush_all();
+    Pp.ppnl(explain_exn e);
     flush_all();
     exit 1)
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index e3431fec..dc3ed452 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -133,6 +133,11 @@ let lookup_modtype mp env =
   with Not_found ->
     failwith ("Unknown module type: "^string_of_mp mp)
 
+let lookup_module mp env =
+  try Environ.lookup_module mp env
+  with Not_found ->
+    failwith ("Unknown module: "^string_of_mp mp)
+
 let rec check_with env mtb with_decl mp=
   match with_decl with
     | With_definition_body (idl,c) ->
@@ -199,7 +204,7 @@ and check_with_mod env mtb (idl,mp1) mp =
 		  SFBmodule msb -> msb
 		| _ -> error_not_a_module l
 	      in
-	      let (_:module_body) = (lookup_module mp1 env) in ()
+	      let (_:module_body) = (Environ.lookup_module mp1 env) in ()
       else
 	    let old = match spec with
 		SFBmodule msb -> msb
diff --git a/configure b/configure
index 589cba6e..f7bdf154 100755
--- a/configure
+++ b/configure
@@ -6,7 +6,7 @@
 # 
 ##################################
 
-VERSION=8.4pl1
+VERSION=8.4pl2
 VOMAGIC=08400
 STATEMAGIC=58400
 DATE=`LC_ALL=C LANG=C date +"%B %Y"`
diff --git a/dev/base_include b/dev/base_include
index ad2a3aec..9a788b7b 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -200,8 +200,8 @@ let pf_e gl s =
 
 (* Set usual printing since the global env is available from the tracer *)
 let _ = Constrextern.in_debugger := false
-let _ = Constrextern.set_debug_global_reference_printer
-  (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+let _ = Constrextern.set_extern_reference
+  (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
 
 open Toplevel
 let go = loop
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0038e78a..c55c4377 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -459,7 +459,7 @@ let encode_path loc prefix mpdir suffix id =
   Qualid (loc, make_qualid
     (make_dirpath (List.rev (id_of_string prefix::dir@suffix))) id)
 
-let raw_string_of_ref loc = function
+let raw_string_of_ref loc _ = function
   | ConstRef cst ->
       let (mp,dir,id) = repr_con cst in
       encode_path loc "CST" (Some (mp,dir)) [] (id_of_label id)
@@ -475,7 +475,7 @@ let raw_string_of_ref loc = function
   | VarRef id ->
       encode_path loc "SECVAR" None [] id
 
-let short_string_of_ref loc = function
+let short_string_of_ref loc _ = function
   | VarRef id -> Ident (loc,id)
   | ConstRef cst -> Ident (loc,id_of_label (pi3 (repr_con cst)))
   | IndRef (kn,0) -> Ident (loc,id_of_label (pi3 (repr_mind kn)))
@@ -491,5 +491,5 @@ let short_string_of_ref loc = function
    pretty-printer should not make calls to the global env since ocamldebug
    runs in a different process and does not have the proper env at hand *)
 let _ = Constrextern.in_debugger := true
-let _ = Constrextern.set_debug_global_reference_printer
+let _ = Constrextern.set_extern_reference
   (if !rawdebug then raw_string_of_ref else short_string_of_ref)
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 07de4daf..94be8318 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -212,6 +212,9 @@ let ignore_break () =
       try Sys.set_signal i (Sys.Signal_handle crash_save)
       with _ -> prerr_endline "Signal ignored (normal if Win32)")
     signals_to_crash;
+  (* We ignore the Ctrl-C, this is required for the Stop button to work,
+     since we will actually send Ctrl-C to all processes sharing
+     our console (including us) *)
   Sys.set_signal Sys.sigint Sys.Signal_ignore
 
 
@@ -902,7 +905,7 @@ object(self)
       if stop#compare start > 0 && is_sentence_end stop#backward_char
       then Some (start,stop)
       else None
-    with Not_found -> None
+    with StartError -> None
 
   method complete_at_offset (offset:int) =
     prerr_endline ("Completion at offset : " ^ string_of_int offset);
@@ -2449,7 +2452,7 @@ let main files =
 	  try configure ~apply:update_notebook_pos ()
 	  with _ -> flash_info "Cannot save preferences"
 	end;
-	reset_revert_timer ()) ~accel:"<Ctrl>," ~stock:`PREFERENCES;
+	reset_revert_timer ()) ~accel:"<Ctrl>comma" ~stock:`PREFERENCES;
       (* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ];
     GAction.add_actions view_actions [
       GAction.add_action "View" ~label:"_View";
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index ebcecc17..aaede465 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -38,6 +38,11 @@ let catch_gtk_messages () =
 
 let () = catch_gtk_messages ()
 
+(* We anticipate a bit the argument parsing and look for -debug *)
+
+let early_set_debug () =
+  Ideutils.debug := List.mem "-debug" (Array.to_list Sys.argv)
+
 (* On win32, we add the directory of coqide to the PATH at launch-time
    (this used to be done in a .bat script). *)
 
@@ -46,47 +51,32 @@ let set_win32_path () =
     (Filename.dirname Sys.executable_name ^ ";" ^
       (try Sys.getenv "PATH" with _ -> ""))
 
-(* On win32, since coqide is now console-free, we re-route stdout/stderr
-   to avoid Sys_error if someone writes to them. We write to a pipe which
-   is never read (by default) or to a temp log file (when in debug mode).
-*)
-
-let reroute_stdout_stderr () =
-  (* We anticipate a bit the argument parsing and look for -debug *)
-  let debug = List.mem "-debug" (Array.to_list Sys.argv) in
-  Ideutils.debug := debug;
-  let out_descr =
-    if debug then
-      let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
-      Coqide.logfile := Some name;
-      Unix.descr_of_out_channel chan
-    else
-      snd (Unix.pipe ())
-  in
+(* On win32, in debug mode we duplicate stdout/stderr in a log file. *)
+
+let log_stdout_stderr () =
+  let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
+  Coqide.logfile := Some name;
+  let out_descr = Unix.descr_of_out_channel chan in
   Unix.set_close_on_exec out_descr;
   Unix.dup2 out_descr Unix.stdout;
   Unix.dup2 out_descr Unix.stderr
 
 (* We also provide specific kill and interrupt functions. *)
 
-(* Since [win32_interrupt] involves some hack about the process console,
-   only one should run at the same time, we simply skip execution of
-   [win32_interrupt] if another instance is already running *)
-
-let ctrl_c_mtx = Mutex.create ()
-
-let ctrl_c_protect f i =
-  if not (Mutex.try_lock ctrl_c_mtx) then ()
-  else try f i; Mutex.unlock ctrl_c_mtx with _ -> Mutex.unlock ctrl_c_mtx
-
 IFDEF WIN32 THEN
 external win32_kill : int -> unit = "win32_kill"
-external win32_interrupt : int -> unit = "win32_interrupt"
+external win32_interrupt_all : unit -> unit = "win32_interrupt_all"
+external win32_hide_console : unit -> unit = "win32_hide_console"
+
 let () =
-  Coq.killer := win32_kill;
-  Coq.interrupter := ctrl_c_protect win32_interrupt;
   set_win32_path ();
-  reroute_stdout_stderr ()
+  Coq.killer := win32_kill;
+  Coq.interrupter := (fun pid -> win32_interrupt_all ());
+  early_set_debug ();
+  if !Ideutils.debug then
+    log_stdout_stderr ()
+  else
+    win32_hide_console ()
 END
 
 IFDEF QUARTZ THEN
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index 67f7e649..47096e6f 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ideutils
 
 let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
 let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0)
diff --git a/ide/ide_win32_stubs.c b/ide/ide_win32_stubs.c
index c09bf37d..c170b1a9 100644
--- a/ide/ide_win32_stubs.c
+++ b/ide/ide_win32_stubs.c
@@ -19,31 +19,33 @@ CAMLprim value win32_kill(value pseudopid) {
   CAMLreturn(Val_unit);
 }
 
-
 /* Win32 emulation of a kill -2 (SIGINT) */
 
-/* This code rely of the fact that coqide is now without initial console.
-   Otherwise, no console creation in win32unix/createprocess.c, hence
-   the same console for coqide and all coqtop, and everybody will be
-   signaled at the same time by the code below. */
+/* For simplicity, we signal all processes sharing a console with coqide.
+   This shouldn't be an issue since currently at most one coqtop is busy
+   at a given time. Earlier, we tried to be more precise via
+   FreeConsole and AttachConsole before generating the Ctrl-C, but
+   that wasn't working so well (see #2869).
+   This code rely now on the fact that coqide is a console app,
+   and that coqide itself ignores Ctrl-C.
+*/
+
+CAMLprim value win32_interrupt_all(value unit) {
+  CAMLparam1(unit);
+  GenerateConsoleCtrlEvent(CTRL_C_EVENT,0);
+  CAMLreturn(Val_unit);
+}
 
-/* Moreover, AttachConsole exists only since WinXP, and GetProcessId
-   since WinXP SP1. For avoiding the GetProcessId, we could adapt code
-   from win32unix/createprocess.c to make it return both the pid and the
-   handle. For avoiding the AttachConsole, I don't know, maybe having
-   an intermediate process between coqide and coqtop ? */
+/* Get rid of the nasty console window (only if we created it) */
 
-CAMLprim value win32_interrupt(value pseudopid) {
-  CAMLparam1(pseudopid);
-  HANDLE h;
+CAMLprim value win32_hide_console (value unit) {
+  CAMLparam1(unit);
   DWORD pid;
-  FreeConsole(); /* Normally unnecessary, just to be sure... */
-  h = (HANDLE)(Long_val(pseudopid));
-  pid = GetProcessId(h);
-  AttachConsole(pid);
-  /* We want to survive the Ctrl-C that will also concerns us */
-  SetConsoleCtrlHandler(NULL,TRUE); /* NULL + TRUE means ignore */
-  GenerateConsoleCtrlEvent(CTRL_C_EVENT,0); /* signal our co-console */
-  FreeConsole();
+  HWND hw = GetConsoleWindow();
+  if (hw != NULL) {
+    GetWindowThreadProcessId(hw, &pid);
+    if (pid == GetCurrentProcessId())
+      ShowWindow(hw, SW_HIDE);
+  }
   CAMLreturn(Val_unit);
 }
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 20b9c2a3..ee529fe0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -137,20 +137,21 @@ let insert_pat_alias loc p = function
 let extern_evar loc n l =
   if !print_evar_arguments then CEvar (loc,n,l) else CEvar (loc,n,None)
 
-let debug_global_reference_printer =
-  ref (fun _ -> failwith "Cannot print a global reference")
+(** We allow customization of the global_reference printer.
+    For instance, in the debugger the tables of global references
+    may be inaccurate *)
 
-let in_debugger = ref false
+let default_extern_reference loc vars r =
+  Qualid (loc,shortest_qualid_of_global vars r)
 
-let set_debug_global_reference_printer f =
-  debug_global_reference_printer := f
+let my_extern_reference = ref default_extern_reference
 
-let extern_reference loc vars r =
-  if !in_debugger then
-    (* Debugger does not have the tables of global reference at hand *)
-    !debug_global_reference_printer loc r
-  else
-    Qualid (loc,shortest_qualid_of_global vars r)
+let set_extern_reference f = my_extern_reference := f
+let get_extern_reference () = !my_extern_reference
+
+let extern_reference loc vars l = !my_extern_reference loc vars l
+
+let in_debugger = ref false
 
 
 (************************************************************************)
@@ -303,10 +304,10 @@ let make_notation_gen loc ntn mknot mkprim destprim l =
 	match decompose_notation_key ntn, l with
 	| [Terminal "-"; Terminal x], [] ->
 	    (try mkprim (loc, Numeral (Bigint.neg (Bigint.of_string x)))
-	     with _ -> mknot (loc,ntn,[]))
+	     with e when Errors.noncritical e -> mknot (loc,ntn,[]))
 	| [Terminal x], [] ->
 	    (try mkprim (loc, Numeral (Bigint.of_string x))
-	     with _ -> mknot (loc,ntn,[]))
+	     with e when Errors.noncritical e -> mknot (loc,ntn,[]))
 	| _ ->
 	    mknot (loc,ntn,l)
 
@@ -816,12 +817,14 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
                 match f with
                 | GRef (_,ref) ->
 	          let subscopes =
-		    try list_skipn n (find_arguments_scope ref) with _ -> [] in
+		    try list_skipn n (find_arguments_scope ref)
+                    with e when Errors.noncritical e -> [] in
 	          let impls =
 		    let impls =
 		      select_impargs_size
 		        (List.length args) (implicits_of_global ref) in
-		    try list_skipn n impls with _ -> [] in
+		    try list_skipn n impls
+                    with e when Errors.noncritical e -> [] in
                   subscopes,impls
                 | _ ->
                   [], [] in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 1a1560e5..55fababd 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -50,9 +50,12 @@ val print_universes : bool ref
 val print_no_symbol : bool ref
 val print_projections : bool ref
 
-(** Debug printing options *)
-val set_debug_global_reference_printer :
-  (loc -> global_reference -> reference) -> unit
+(** Customization of the global_reference printer *)
+val set_extern_reference :
+  (loc -> Idset.t -> global_reference -> reference) -> unit
+val get_extern_reference :
+  unit -> (loc -> Idset.t -> global_reference -> reference)
+
 val in_debugger : bool ref
 
 (** This governs printing of implicit arguments. If [with_implicits] is
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 81e4501a..e806686a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -650,7 +650,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
 	let scopes = find_arguments_scope ref in
 	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
 	GRef (loc, ref), impls, scopes, []
-      with _ ->
+      with e when Errors.noncritical e ->
 	(* [id] a goal variable *)
 	GVar (loc,id), [], [], []
 
@@ -716,7 +716,7 @@ let intern_applied_reference intern env namedctx lvar args = function
       try
 	let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in
 	find_appl_head_data r, args2
-      with e ->
+      with e when Errors.noncritical e ->
 	(* Extra allowance for non globalizing functions *)
 	if !interning_grammar || env.unb then
 	  (GVar (loc,id), [], [], []),args
@@ -969,15 +969,15 @@ let sort_fields mode loc l completer =
 		    | [] -> anomaly "Number of projections mismatch"
 		    | (_, regular)::tm ->
 		       let boolean = not regular in
-		       if ConstRef name = global_reference_of_reference refer
-		       then
+                       (match global_reference_of_reference refer with
+                       | ConstRef name' when eq_constant name name' ->
 			 if boolean && mode then
 			   user_err_loc (loc, "", str"No local fields allowed in a record construction.")
 			 else build_patt b tm (i + 1) (i, snd acc) (* we found it *)
-		       else
+                       | _ ->
 			  build_patt b tm (if boolean&&mode then i else i + 1)
 			    (if boolean && mode then acc
-			     else fst acc, (i, ConstRef name) :: snd acc))
+			     else fst acc, (i, ConstRef name) :: snd acc)))
 	      | None :: b-> (* we don't want anonymous fields *)
 		 if mode then
 		   user_err_loc (loc, "", str "This record contains anonymous fields.")
@@ -1009,7 +1009,7 @@ let sort_fields mode loc l completer =
 			 (loc, "",
 			  str "This record contains fields of different records.")
 		   | (i, a) :: b->
-		       if glob_refer = a
+		       if eq_gr glob_refer a
 		       then (i,List.rev_append acc l)
 		       else add_patt b ((i,a)::acc)
 	         in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 9950178c..2c000258 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -88,8 +88,8 @@ let is_freevar ids env x =
     if Idset.mem x ids then false
     else
       try ignore(Environ.lookup_named x env) ; false
-      with _ -> not (is_global x)
-  with _ -> true
+      with e when Errors.noncritical e -> not (is_global x)
+  with e when Errors.noncritical e -> true
 
 (* Auxiliary functions for the inference of implicitly quantified variables. *)
 
diff --git a/interp/notation.ml b/interp/notation.ml
index e3fb5d5e..03fa23a3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -838,4 +838,4 @@ let _ =
 let with_notation_protection f x =
   let fs = freeze () in
   try let a = f x in unfreeze fs; a
-  with e -> unfreeze fs; raise e
+  with reraise -> unfreeze fs; raise reraise
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 8d09cbd7..9c9f6a57 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -190,7 +190,9 @@ and eval_to_patch env (buff,pl,fv) =
 and val_of_constr env c =
   let (_,fun_code,_ as ccfv) =
     try compile env c
-    with e -> print_string "can not compile \n";Format.print_flush();raise e in
+    with reraise ->
+      print_string "can not compile \n";Format.print_flush();raise reraise
+  in
   eval_to_patch env (to_memory ccfv)
 
 let set_transparent_const kn =
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 15a48e1c..9aeaf110 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -83,13 +83,14 @@ let string_of_hint = function
   | Equiv kn -> string_of_kn kn
 
 let debug_string_of_delta resolve =
-  let kn_to_string kn hint s =
-    s^", "^(string_of_kn kn)^"=>"^(string_of_hint hint)
+  let kn_to_string kn hint l =
+    (string_of_kn kn ^ "=>" ^ string_of_hint hint) :: l
   in
-  let mp_to_string mp mp' s =
-    s^", "^(string_of_mp mp)^"=>"^(string_of_mp mp')
+  let mp_to_string mp mp' l =
+    (string_of_mp mp ^ "=>" ^ string_of_mp mp') :: l
   in
-  Deltamap.fold mp_to_string kn_to_string resolve ""
+  let l = Deltamap.fold mp_to_string kn_to_string resolve [] in
+  String.concat ", " (List.rev l)
 
 let list_contents sub =
   let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in
@@ -173,7 +174,7 @@ let solve_delta_kn resolve kn =
 
 let kn_of_delta resolve kn =
   try solve_delta_kn resolve kn
-  with _ -> kn
+  with e when Errors.noncritical e -> kn
 
 let constant_of_delta_kn resolve kn =
   constant_of_kn_equiv kn (kn_of_delta resolve kn)
@@ -182,7 +183,7 @@ let gen_of_delta resolve x kn fix_can =
   try
     let new_kn = solve_delta_kn resolve kn in
     if kn == new_kn then x else fix_can new_kn
-  with _ -> x
+  with e when Errors.noncritical e -> x
 
 let constant_of_delta resolve con =
   let kn = user_con con in
@@ -223,8 +224,10 @@ let constant_of_delta_with_inline resolve con =
   let kn1,kn2 = canonical_con con,user_con con in
   try find_inline_of_delta kn2 resolve
   with Not_found ->
-    try find_inline_of_delta kn1 resolve
-    with Not_found -> None
+    if kn1 == kn2 then None
+    else
+      try find_inline_of_delta kn1 resolve
+      with Not_found -> None
 
 let subst_mp0 sub mp = (* 's like subst *)
  let rec aux mp =
@@ -272,7 +275,9 @@ type sideconstantsubst =
   | Canonical
 
 let gen_subst_mp f sub mp1 mp2 =
-  match subst_mp0 sub mp1, subst_mp0 sub mp2 with
+  let o1 = subst_mp0 sub mp1 in
+  let o2 = if mp1 == mp2 then o1 else subst_mp0 sub mp2 in
+  match o1, o2 with
     | None, None -> raise No_subst
     | Some (mp',resolve), None -> User, (f mp' mp2), resolve
     | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve
diff --git a/kernel/modops.ml b/kernel/modops.ml
index af32288c..a81f868e 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -33,7 +33,7 @@ type signature_mismatch_error =
   | NotConvertibleInductiveField of identifier
   | NotConvertibleConstructorField of identifier
   | NotConvertibleBodyField
-  | NotConvertibleTypeField
+  | NotConvertibleTypeField of env * types * types
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
   | FiniteInductiveFieldExpected of bool
diff --git a/kernel/modops.mli b/kernel/modops.mli
index d03d61bd..daea3258 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -9,6 +9,7 @@
 open Util
 open Names
 open Univ
+open Term
 open Environ
 open Declarations
 open Entries
@@ -60,7 +61,7 @@ type signature_mismatch_error =
   | NotConvertibleInductiveField of identifier
   | NotConvertibleConstructorField of identifier
   | NotConvertibleBodyField
-  | NotConvertibleTypeField
+  | NotConvertibleTypeField of env * types * types
   | NotSameConstructorNamesField
   | NotSameInductiveNameInBlockField
   | FiniteInductiveFieldExpected of bool
diff --git a/kernel/names.ml b/kernel/names.ml
index 17bda124..8c228404 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -205,7 +205,9 @@ type constant = kernel_name*kernel_name
 let constant_of_kn kn = (kn,kn)
 let constant_of_kn_equiv kn1 kn2 = (kn1,kn2)
 let make_con mp dir l = constant_of_kn (mp,dir,l)
-let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
+let make_con_equiv mp1 mp2 dir l =
+  if mp1 == mp2 then make_con mp1 dir l
+  else ((mp1,dir,l),(mp2,dir,l))
 let canonical_con con = snd con
 let user_con con = fst con
 let repr_con con = fst con
@@ -263,8 +265,10 @@ let constr_modpath c = ind_modpath (fst c)
 
 let mind_of_kn kn = (kn,kn)
 let mind_of_kn_equiv kn1 kn2 = (kn1,kn2)
-let make_mind mp dir l = ((mp,dir,l),(mp,dir,l))
-let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l))
+let make_mind mp dir l = mind_of_kn (mp,dir,l)
+let make_mind_equiv mp1 mp2 dir l =
+  if mp1 == mp2 then make_mind mp1 dir l
+  else ((mp1,dir,l),(mp2,dir,l))
 let canonical_mind mind = snd mind
 let user_mind mind = fst mind
 let repr_mind mind = fst mind
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 6c08c34c..f0a3292c 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -90,7 +90,7 @@ let push_rel d env =
 
 let lookup_rel_val n env =
   try List.nth env.env_rel_val (n - 1)
-  with _ -> raise Not_found
+  with e when Errors.noncritical e -> raise Not_found
 
 let env_of_rel n env =
   { env with
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1d606782..ec891e13 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -477,7 +477,7 @@ let end_module l restype senv =
    in
    let str = match sign with
      | SEBstruct(str_l) -> str_l
-     | _ -> error ("You cannot Include a high-order structure.")
+     | _ -> error ("You cannot Include a higher-order structure.")
    in
    let senv = update_resolver (add_delta_resolver resolver) senv
    in
@@ -873,7 +873,8 @@ end = struct
 	  let k = key_of_lazy_constr k in
 	  let access key =
 	    try (Lazy.force table).(key)
-	    with _ -> error "Error while retrieving an opaque body"
+	    with e when Errors.noncritical e ->
+              error "Error while retrieving an opaque body"
 	  in
 	  match load_proof with
 	    | Flags.Force ->
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index e2c5f48c..c809572a 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -219,6 +219,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
   let check_conv cst f = check_conv_error error cst f in
   let check_type cst env t1 t2 =
 
+    let err = NotConvertibleTypeField (env, t1, t2) in
+
     (* If the type of a constant is generated, it may mention
        non-variable algebraic universes that the general conversion
        algorithm is not ready to handle. Anyway, generated types of
@@ -257,12 +259,12 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
                  (the user has to use an explicit type in the interface *)
                 error NoTypeConstraintExpected
           with NotArity ->
-            error NotConvertibleTypeField end
+            error err end
         | _ ->
 	  t1,t2
       else
         (t1,t2) in
-    check_conv NotConvertibleTypeField cst conv_leq env t1 t2
+    check_conv err cst conv_leq env t1 t2
   in
 
   match info1 with
@@ -301,7 +303,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       if constant_has_body cb2 then error DefinitionFieldExpected;
       let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2
+      let error = NotConvertibleTypeField (env, arity1, typ2) in
+       check_conv error cst conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
       ignore (Util.error (
        "The kernel does not recognize yet that a parameter can be " ^
@@ -312,7 +315,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       if constant_has_body cb2 then error DefinitionFieldExpected;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
-       check_conv NotConvertibleTypeField cst conv env ty1 ty2
+      let error = NotConvertibleTypeField (env, ty1, ty2) in
+       check_conv error cst conv env ty1 ty2
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module None msb1 in
diff --git a/lib/envars.ml b/lib/envars.ml
index 4ec68a27..c672d30c 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -23,6 +23,8 @@ let _ =
   if Coq_config.arch = "win32" then
     Unix.putenv "PATH" (coqbin ^ ";" ^ System.getenv_else "PATH" "")
 
+let exe s = s ^ Coq_config.exec_extension
+
 let reldir instdir testfile oth =
   let rpath = if Coq_config.local then [] else instdir in
   let out = List.fold_left Filename.concat coqroot rpath in
@@ -87,19 +89,19 @@ let rec which l f =
 	else which tl f
 
 let guess_camlbin () =
-  let path = try Sys.getenv "PATH" with _ -> raise Not_found in
+  let path = Sys.getenv "PATH" in (* may raise Not_found *)
   let lpath = path_to_list path in
-    which lpath "ocamlc"
+    which lpath (exe "ocamlc")
 
 let guess_camlp4bin () =
-  let path = try Sys.getenv "PATH" with _ -> raise Not_found in
+  let path = Sys.getenv "PATH" in (* may raise Not_found *)
   let lpath = path_to_list path in
-    which lpath Coq_config.camlp4
+    which lpath (exe Coq_config.camlp4)
 
 let camlbin () =
   if !Flags.camlbin_spec then !Flags.camlbin else
     if !Flags.boot then Coq_config.camlbin else
-      try guess_camlbin () with _ -> Coq_config.camlbin
+      try guess_camlbin () with e when e <> Sys.Break -> Coq_config.camlbin
 
 let camllib () =
   if !Flags.boot
@@ -113,9 +115,10 @@ let camllib () =
 let camlp4bin () =
   if !Flags.camlp4bin_spec then !Flags.camlp4bin else
     if !Flags.boot then Coq_config.camlp4bin else
-      try guess_camlp4bin () with _ -> let cb = camlbin () in
-				       if Sys.file_exists (Filename.concat cb Coq_config.camlp4) then cb
-				       else Coq_config.camlp4bin
+      try guess_camlp4bin () with e when e <> Sys.Break ->
+        let cb = camlbin () in
+	if Sys.file_exists (Filename.concat cb (exe Coq_config.camlp4)) then cb
+	else Coq_config.camlp4bin
 
 let camlp4lib () =
   if !Flags.boot
diff --git a/lib/errors.ml b/lib/errors.ml
index 3b5e6770..6affea23 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -28,7 +28,7 @@ let rec print_gen bottom stk e =
     try h e
     with
     | Unhandled -> print_gen bottom stk' e
-    | e' -> print_gen bottom stk' e'
+    | any -> print_gen bottom stk' any
 
 (** Only anomalies should reach the bottom of the handler stack.
     In usual situation, the [handle_stack] is treated as it if was always
@@ -66,3 +66,14 @@ let _ = register_handler begin function
   | _ -> raise Unhandled
 end
 
+(** Critical exceptions shouldn't be catched and ignored by mistake
+    by inner functions during a [vernacinterp]. They should be handled
+    only at the very end of interp, to be displayed to the user. *)
+
+(** NB: in the 8.4 branch, for maximal compatibility, anomalies
+    are considered non-critical *)
+
+let noncritical = function
+  | Sys.Break | Out_of_memory | Stack_overflow -> false
+  | _ -> true
+
diff --git a/lib/errors.mli b/lib/errors.mli
index eb7fde8e..ae4d0b85 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -39,3 +39,11 @@ val print_no_report : exn -> Pp.std_ppcmds
 (** Same as [print], except that anomalies are not printed but re-raised
     (used for the Fail command) *)
 val print_no_anomaly : exn -> Pp.std_ppcmds
+
+(** Critical exceptions shouldn't be catched and ignored by mistake
+    by inner functions during a [vernacinterp]. They should be handled
+    only in [Toplevel.do_vernac] (or Ideslave), to be displayed to the user.
+    Typical example: [Sys.Break]. In the 8.4 branch, for maximal
+    compatibility, anomalies are not considered as critical...
+*)
+val noncritical : exn -> bool
diff --git a/lib/flags.ml b/lib/flags.ml
index 3474573e..32c68b25 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -9,12 +9,12 @@
 let with_option o f x =
   let old = !o in o:=true;
   try let r = f x in o := old; r
-  with e -> o := old; raise e
+  with reraise -> o := old; raise reraise
 
 let without_option o f x =
   let old = !o in o:=false;
   try let r = f x in o := old; r
-  with e -> o := old; raise e
+  with reraise -> o := old; raise reraise
 
 let boot = ref false
 
diff --git a/lib/hashtbl_alt.ml b/lib/hashtbl_alt.ml
index 2780afe8..bb2252da 100644
--- a/lib/hashtbl_alt.ml
+++ b/lib/hashtbl_alt.ml
@@ -89,7 +89,7 @@ module Make (E : Hashtype) =
 		match rest2 with
 		  | Empty -> add hash key; key
 		  | Cons (k3, h3, rest3) ->
-		    if hash == h2 && E.equals key k3 then k3
+		    if hash == h3 && E.equals key k3 then k3
 		    else find_rec hash key rest3
 
 end
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 7777d091..569a028f 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -279,7 +279,7 @@ let pp_dirs ft =
     try
       Stream.iter pp_dir dirstream; com_brk ft
     with
-      | e -> Format.pp_print_flush ft () ; raise e
+      | reraise -> Format.pp_print_flush ft () ; raise reraise
 
 
 (* pretty print on stdout and stderr *)
diff --git a/lib/profile.ml b/lib/profile.ml
index 2472d75d..39e08721 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -260,7 +260,7 @@ let time_overhead_B_C () =
       let _dw = dummy_spent_alloc () in
       let _dt = get_time () in
       ()
-    with _ -> assert false
+    with e when e <> Sys.Break -> assert false
   done;
   let after = get_time () in
   let beforeloop =  get_time () in
@@ -390,7 +390,7 @@ let profile1 e f a =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -403,7 +403,7 @@ let profile1 e f a =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile2 e f a b =
   let dw = spent_alloc () in
@@ -432,7 +432,7 @@ let profile2 e f a b =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -445,7 +445,7 @@ let profile2 e f a b =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile3 e f a b c =
   let dw = spent_alloc () in
@@ -474,7 +474,7 @@ let profile3 e f a b c =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -487,7 +487,7 @@ let profile3 e f a b c =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile4 e f a b c d =
   let dw = spent_alloc () in
@@ -516,7 +516,7 @@ let profile4 e f a b c d =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -529,7 +529,7 @@ let profile4 e f a b c d =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile5 e f a b c d g =
   let dw = spent_alloc () in
@@ -558,7 +558,7 @@ let profile5 e f a b c d g =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -571,7 +571,7 @@ let profile5 e f a b c d g =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile6 e f a b c d g h =
   let dw = spent_alloc () in
@@ -600,7 +600,7 @@ let profile6 e f a b c d g h =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -613,7 +613,7 @@ let profile6 e f a b c d g h =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 let profile7 e f a b c d g h i =
   let dw = spent_alloc () in
@@ -642,7 +642,7 @@ let profile7 e f a b c d g h i =
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
     r
-  with exn ->
+  with reraise ->
     let dw = spent_alloc () in
     let dt = get_time () - t in
     e.tottime <- e.tottime + dt; e.owntime <- e.owntime + dt;
@@ -655,7 +655,7 @@ let profile7 e f a b c d g h i =
     if not (p==e) then
       (match !stack with [] -> assert false | _::s -> stack := s);
     last_alloc := get_alloc ();
-    raise exn
+    raise reraise
 
 (* Some utilities to compute the logical and physical sizes and depth
    of ML objects *)
diff --git a/lib/store.ml b/lib/store.ml
index bc1b335f..28eb65c8 100644
--- a/lib/store.ml
+++ b/lib/store.ml
@@ -53,7 +53,7 @@ let field () =
   in
   let get s =
     try Some (Obj.obj (Util.Intmap.find fid s))
-    with _ -> None
+    with Not_found -> None
   in
   let remove s =
     Util.Intmap.remove fid s
diff --git a/lib/system.ml b/lib/system.ml
index a99c29f2..ae637708 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -140,7 +140,8 @@ let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
 
 let ok_dirname f =
   f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) &&
-  try ignore (check_ident f); true with _ -> false
+  try ignore (check_ident f); true
+  with e when e <> Sys.Break -> false
 
 let all_subdirs ~unix_path:root =
   let l = ref [] in
@@ -223,17 +224,22 @@ let file_readable_p name =
   try access name [R_OK];true with Unix_error (_, _, _) -> false
 
 let open_trapping_failure name =
-  try open_out_bin name with _ -> error ("Can't open " ^ name)
+  try open_out_bin name
+  with e when e <> Sys.Break -> error ("Can't open " ^ name)
 
 let try_remove filename =
   try Sys.remove filename
-  with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++
-                   str filename ++ str" which is corrupted!" )
+  with e when e <> Sys.Break ->
+    msgnl (str"Warning: " ++ str"Could not remove file " ++
+             str filename ++ str" which is corrupted!" )
 
 let marshal_out ch v = Marshal.to_channel ch v []
-let marshal_in ch =
+let marshal_in filename ch =
   try Marshal.from_channel ch
-  with End_of_file -> error "corrupted file: reached end of file"
+  with
+    | End_of_file -> error "corrupted file: reached end of file"
+    | Failure _ (* e.g. "truncated object" *) ->
+        error (filename ^ " is corrupted, try to rebuild it.")
 
 exception Bad_magic_number of string
 
@@ -259,14 +265,14 @@ let extern_intern ?(warn=true) magic suffix =
       try
         marshal_out channel val_0;
         close_out channel
-      with e ->
-	begin try_remove filename; raise e end
+      with reraise ->
+	begin try_remove filename; raise reraise end
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name =
     try
       let _,filename = find_file_in_path ~warn paths (make_suffix name suffix) in
       let channel = raw_intern filename in
-      let v = marshal_in channel in
+      let v = marshal_in filename channel in
       close_in channel;
       v
     with Sys_error s ->
diff --git a/lib/system.mli b/lib/system.mli
index 4a79b874..d8420e7d 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -47,7 +47,7 @@ val find_file_in_path :
   when the check fails, with the full file name. *)
 
 val marshal_out : out_channel -> 'a -> unit
-val marshal_in : in_channel -> 'a
+val marshal_in : string -> in_channel -> 'a
 
 exception Bad_magic_number of string
 
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
index 19bab4f6..600796f7 100644
--- a/lib/xml_parser.ml
+++ b/lib/xml_parser.ml
@@ -175,7 +175,7 @@ let do_parse xparser source =
 		if xparser.check_eof && pop s <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
 		Xml_lexer.close source;
 		x
-	with e ->
+	with e when e <> Sys.Break ->
 	  Xml_lexer.close source;
 	  raise (!xml_error (error_of_exn stk e) source)
 
@@ -190,9 +190,9 @@ let parse p = function
 			close_in ch;
 			x
 		with
-			e ->
+			reraise ->
 				close_in ch;
-				raise e
+				raise reraise
 
 
 let error_msg = function
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 80da9e73..db7b8915 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -990,9 +990,9 @@ let declare_include_ interp_struct me_asts =
 let protect_summaries f =
   let fs = Summary.freeze_summaries () in
   try f fs
-  with e ->
+  with reraise ->
     (* Something wrong: undo the whole process *)
-    Summary.unfreeze_summaries fs; raise e
+    Summary.unfreeze_summaries fs; raise reraise
 
 let declare_include interp_struct me_asts =
   protect_summaries
diff --git a/library/heads.ml b/library/heads.ml
index b860dc2a..c33ea9b1 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -88,7 +88,7 @@ let kind_of_head env t =
   | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
   | Cast (c,_,_) -> aux k l c b
   | Lambda (_,_,c) when l = [] -> assert (not b); aux (k+1) [] c b
-  | Lambda (_,_,c) -> aux (k+1) (List.tl l) (subst1 (List.hd l) c) b
+  | Lambda (_,_,c) -> aux k (List.tl l) (subst1 (List.hd l) c) b
   | LetIn _ -> assert false
   | Meta _ | Evar _ -> NotImmediatelyComputableHead
   | App (c,al) -> aux k (Array.to_list al @ l) c b
diff --git a/library/impargs.ml b/library/impargs.ml
index c79edb99..930b8f09 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -74,9 +74,9 @@ let with_implicits flags f x =
     let rslt = f x in
     implicit_args := oflags;
     rslt
-  with e -> begin
+  with reraise -> begin
     implicit_args := oflags;
-    raise e
+    raise reraise
   end
 
 let set_maximality imps b =
diff --git a/library/library.ml b/library/library.ml
index 30e7b675..c857fc86 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -368,14 +368,14 @@ let explain_locate_library_error qid = function
 let try_locate_absolute_library dir =
   try
     locate_absolute_library dir
-  with e ->
+  with e when Errors.noncritical e ->
     explain_locate_library_error (qualid_of_dirpath dir) e
 
 let try_locate_qualified_library (loc,qid) =
   try
     let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
     dir,f
-  with e ->
+  with e when Errors.noncritical e ->
     explain_locate_library_error qid e
 
 
@@ -398,20 +398,20 @@ let fetch_opaque_table (f,pos,digest) =
   try
     let ch = System.with_magic_number_check raw_intern_library f in
     seek_in ch pos;
-    if System.marshal_in ch <> digest then failwith "File changed!";
-    let table = (System.marshal_in ch : LightenLibrary.table) in
+    if System.marshal_in f ch <> digest then failwith "File changed!";
+    let table = (System.marshal_in f ch : LightenLibrary.table) in
     close_in ch;
     table
-  with _ ->
+  with e when Errors.noncritical e ->
     error
       ("The file "^f^" is inaccessible or has changed,\n" ^
        "cannot load some opaque constant bodies in it.\n")
 
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
-  let lmd = System.marshal_in ch in
+  let lmd = System.marshal_in f ch in
   let pos = pos_in ch in
-  let digest = System.marshal_in ch in
+  let digest = System.marshal_in f ch in
   let table = lazy (fetch_opaque_table (f,pos,digest)) in
   register_library_filename lmd.md_name f;
   let library = mk_library lmd table digest in
@@ -655,7 +655,8 @@ let save_library_to dir f =
     System.marshal_out ch di;
     System.marshal_out ch table;
     close_out ch
-  with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e
+  with reraise ->
+    warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise
 
 (************************************************************************)
 (*s Display the memory use of a library. *)
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 184985b5..7a214bcd 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -393,14 +393,17 @@ let extra_rules () = begin
        Cmd (S [P w32res;A "--input-format";A "rc";A "--input";P rc;
 	       A "--output-format";A "coff";A "--output"; Px o]));
 
-(** The windows version of Coqide is now a console-free win32 app,
-    which moreover contains the Coq icon. If necessary, the mkwinapp
-    tool can be used later to restore or suppress the console of Coqide. *)
+(** Embed the Coq icon inside the windows version of Coqide *)
 
   if w32 then dep ["link"; "ocaml"; "program"; "ide"] [w32ico];
-
-  if w32 then flag ["link"; "ocaml"; "program"; "ide"]
-    (S [A "-ccopt"; A "-link -Wl,-subsystem,windows"; P w32ico]);
+  if w32 then flag ["link"; "ocaml"; "program"; "ide"] (P w32ico);
+
+(** Ealier we tried to make Coqide a console-free win32 app,
+    but that was troublesome (unavailable stdout/stderr, issues
+    with the stop button,...). If somebody really want to try again,
+    the extra args to add are :
+      [A "-ccopt"; A "-link -Wl,-subsystem,windows"]
+    Other solution: use the mkwinapp tool. *)
 
 (** The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/".
     Let's tweak that... *)
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 1888ef17..214a6b98 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -146,7 +146,7 @@ let possibly_empty_subentries loc (prods,act) =
     (* an exception rather than returning a value; *)
     (* declares loc because some code can refer to it; *)
     (* ensures loc is used to avoid "unused variable" warning *)
-    (true, <:expr< try Some $aux prods$ with [ _ -> None ] >>)
+    (true, <:expr< try Some $aux prods$ with [ e when Errors.noncritical e -> None ] >>)
   else
     (* Static optimisation *)
     (false, aux prods)
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index c68ba137..12359776 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -365,4 +365,4 @@ let _ =
 let with_grammar_rule_protection f x =
   let fs = freeze () in
   try let a = f x in unfreeze fs; a
-  with e -> unfreeze fs; raise e
+  with reraise -> unfreeze fs; raise reraise
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d265729a..1609e541 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -126,7 +126,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
 let induction_arg_of_constr (c,lbind as clbind) =
   if lbind = NoBindings then
     try ElimOnIdent (constr_loc c,snd(coerce_to_id c))
-    with _ -> ElimOnConstr clbind
+    with e when Errors.noncritical e -> ElimOnConstr clbind
   else ElimOnConstr clbind
 
 let mkTacCase with_evar = function
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 9dd0e369..869674f4 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -104,7 +104,8 @@ let get_xml_sort al = sort_of_cdata (get_xml_attr "value" al)
 
 let get_xml_inductive_kn al =
   inductive_of_cdata (* uriType apparent synonym of uri *)
-    (try get_xml_attr "uri" al with _ -> get_xml_attr "uriType" al)
+    (try get_xml_attr "uri" al
+     with e when Errors.noncritical e -> get_xml_attr "uriType" al)
 
 let get_xml_constant al = constant_of_cdata (get_xml_attr "uri" al)
 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index d3eb40d0..99e10908 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -273,7 +273,9 @@ let print_inductive_implicit_args =
 
 let print_inductive_renames =
   print_args_data_of_inductive_ids
-    (fun r -> try List.hd (Arguments_renaming.arguments_names r) with _ -> [])
+    (fun r ->
+      try List.hd (Arguments_renaming.arguments_names r)
+      with e when Errors.noncritical e -> [])
     ((<>) Anonymous)
     print_renames_list
 
@@ -737,7 +739,7 @@ let print_coercions () =
 let index_of_class cl =
   try
     fst (class_info cl)
-  with _ ->
+  with e when Errors.noncritical e ->
     errorlabstrm "index_of_class"
       (pr_class cl ++ spc() ++ str "not a defined class.")
 
@@ -747,7 +749,7 @@ let print_path_between cls clt =
   let p =
     try
       lookup_path_between_class (i,j)
-    with _ ->
+    with e when Errors.noncritical e ->
       errorlabstrm "index_cl_of_id"
         (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
 	 ++ str ".")
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 9f0cb00d..29ebe4fa 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -24,6 +24,7 @@ open Pfedit
 open Ppconstr
 open Constrextern
 open Tacexpr
+open Declarations
 
 open Store.Field
 
@@ -118,6 +119,63 @@ let pr_sort s = pr_glob_sort (extern_sort s)
 
 let _ = Termops.set_print_constr pr_lconstr_env
 
+
+(** Term printers resilient to [Nametab] errors *)
+
+(** When the nametab isn't up-to-date, the term printers above
+    could raise [Not_found] during [Nametab.shortest_qualid_of_global].
+    In this case, we build here a fully-qualified name based upon
+    the kernel modpath and label of constants, and the idents in
+    the [mutual_inductive_body] for the inductives and constructors
+    (needs an environment for this). *)
+
+let id_of_global env = function
+  | ConstRef kn -> id_of_label (con_label kn)
+  | IndRef (kn,0) -> id_of_label (mind_label kn)
+  | IndRef (kn,i) ->
+    (Environ.lookup_mind kn env).mind_packets.(i).mind_typename
+  | ConstructRef ((kn,i),j) ->
+    (Environ.lookup_mind kn env).mind_packets.(i).mind_consnames.(j-1)
+  | VarRef v -> v
+
+let cons_dirpath id dp = make_dirpath (id :: repr_dirpath dp)
+
+let rec dirpath_of_mp = function
+  | MPfile sl -> sl
+  | MPbound uid -> make_dirpath [id_of_mbid uid]
+  | MPdot (mp,l) -> cons_dirpath (id_of_label l) (dirpath_of_mp mp)
+
+let dirpath_of_global = function
+  | ConstRef kn -> dirpath_of_mp (con_modpath kn)
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+    dirpath_of_mp (mind_modpath kn)
+  | VarRef _ -> empty_dirpath
+
+let qualid_of_global env r =
+  Libnames.make_qualid (dirpath_of_global r) (id_of_global env r)
+
+let safe_gen f env c =
+  let orig_extern_ref = Constrextern.get_extern_reference () in
+  let extern_ref loc vars r =
+    try orig_extern_ref loc vars r
+    with e when Errors.noncritical e ->
+      Libnames.Qualid (loc, qualid_of_global env r)
+  in
+  Constrextern.set_extern_reference extern_ref;
+  try
+    let p = f env c in
+    Constrextern.set_extern_reference orig_extern_ref;
+    p
+  with e when Errors.noncritical e ->
+    Constrextern.set_extern_reference orig_extern_ref;
+    str "??"
+
+let safe_pr_lconstr_env = safe_gen pr_lconstr_env
+let safe_pr_constr_env = safe_gen pr_constr_env
+let safe_pr_lconstr t = safe_pr_lconstr_env (Global.env()) t
+let safe_pr_constr t = safe_pr_constr_env (Global.env()) t
+
+
 (**********************************************************************)
 (* Global references *)
 
@@ -389,7 +447,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
 	| None ->
 	    let exl = Evarutil.non_instantiated sigma in
 	    if exl = [] then
-	      (str"No more subgoals."
+	      (str"No more subgoals." ++ fnl ()
 	       ++ emacs_print_dependent_evars sigma seeds)
 	    else
 	      let pei = pr_evars_int 1 exl in
@@ -415,7 +473,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
       v 0 (
 	int(List.length rest+1) ++ str" subgoals" ++
           str (emacs_str ", subgoal 1") ++ pr_goal_tag g1 ++ cut ()
-	++ goals
+	++ goals ++ fnl ()
 	++ emacs_print_dependent_evars sigma seeds
       )
   | g1::rest,a::l ->
@@ -589,7 +647,7 @@ let pr_assumptionset env s =
 	str (string_of_mp mp ^ "." ^ string_of_label lab)
     in
     let safe_pr_ltype typ =
-      try str " : " ++ pr_ltype typ with _ -> mt ()
+      try str " : " ++ pr_ltype typ with e when Errors.noncritical e -> mt ()
     in
     let (vars,axioms,opaque) =
       ContextObjectMap.fold (fun t typ r ->
@@ -647,7 +705,6 @@ let pr_instance_gmap insts =
 
 (** Inductive declarations *)
 
-open Declarations
 open Termops
 open Reduction
 open Inductive
diff --git a/parsing/printer.mli b/parsing/printer.mli
index a034f0ed..3abe90e7 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -31,6 +31,17 @@ val pr_lconstr             : constr -> std_ppcmds
 val pr_constr_env          : env -> constr -> std_ppcmds
 val pr_constr              : constr -> std_ppcmds
 
+(** Same, but resilient to [Nametab] errors. Prints fully-qualified
+    names when [shortest_qualid_of_global] has failed. Prints "??"
+    in case of remaining issues (such as reference not in env). *)
+
+val safe_pr_lconstr_env         : env -> constr -> std_ppcmds
+val safe_pr_lconstr             : constr -> std_ppcmds
+
+val safe_pr_constr_env          : env -> constr -> std_ppcmds
+val safe_pr_constr              : constr -> std_ppcmds
+
+
 val pr_open_constr_env     : env -> open_constr -> std_ppcmds
 val pr_open_constr         : open_constr -> std_ppcmds
 
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index b4a8fdfd..b46cf42d 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -68,12 +68,17 @@ let print_kn locals kn =
 	with
 	    Not_found -> print_modpath locals kn
 
+(** Each time we have to print a non-globally visible structure,
+    we place its elements in a fake fresh namespace. *)
+
+let mk_fake_top =
+  let r = ref 0 in
+  fun () -> incr r; id_of_string ("FAKETOP"^(string_of_int !r))
+
 let nametab_register_dir mp =
-  let id = id_of_string "FAKETOP" in
-  let fp = Libnames.make_path empty_dirpath id in
+  let id = mk_fake_top () in
   let dir = make_dirpath [id] in
-  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)));
-  fp
+  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)))
 
 (** Nota: the [global_reference] we register in the nametab below
     might differ from internal ones, since we cannot recreate here
@@ -81,9 +86,10 @@ let nametab_register_dir mp =
     the user names. This works nonetheless since we search now
     [Nametab.the_globrevtab] modulo user name. *)
 
-let nametab_register_body mp fp (l,body) =
+let nametab_register_body mp dir (l,body) =
   let push id ref =
-    Nametab.push (Nametab.Until 1) (make_path (dirpath fp) id) ref
+    Nametab.push (Nametab.Until (1+List.length (repr_dirpath dir)))
+      (make_path dir id) ref
   in
   match body with
     | SFBmodule _ -> () (* TODO *)
@@ -99,6 +105,27 @@ let nametab_register_body mp fp (l,body) =
 	    mip.mind_consnames)
 	mib.mind_packets
 
+let nametab_register_module_body mp struc =
+  (* If [mp] is a globally visible module, we simply import it *)
+  try Declaremods.really_import_module mp
+  with Not_found ->
+    (* Otherwise we try to emulate an import by playing with nametab *)
+    nametab_register_dir mp;
+    List.iter (nametab_register_body mp empty_dirpath) struc
+
+let nametab_register_module_param mbid seb =
+  (* For algebraic seb, we use a Declaremods function that converts into mse *)
+  try Declaremods.process_module_seb_binding mbid seb
+  with e when Errors.noncritical e ->
+    (* Otherwise, for expanded structure, we try to play with the nametab *)
+    match seb with
+      | SEBstruct struc ->
+        let mp = MPbound mbid in
+        let dir = make_dirpath [id_of_mbid mbid] in
+        nametab_register_dir mp;
+        List.iter (nametab_register_body mp dir) struc
+      | _ -> ()
+
 let print_body is_impl env mp (l,body) =
   let name = str (string_of_label l) in
   hov 2 (match body with
@@ -126,19 +153,11 @@ let print_body is_impl env mp (l,body) =
       try
 	let env = Option.get env in
 	Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib
-      with _ ->
+      with e when Errors.noncritical e ->
 	(if mib.mind_finite then str "Inductive " else str "CoInductive")
 	++ name)
 
 let print_struct is_impl env mp struc =
-  begin
-    (* If [mp] is a globally visible module, we simply import it *)
-    try Declaremods.really_import_module mp
-    with _ ->
-    (* Otherwise we try to emulate an import by playing with nametab *)
-      let fp = nametab_register_dir mp in
-      List.iter (nametab_register_body mp fp) struc
-  end;
   prlist_with_sep spc (print_body is_impl env mp) struc
 
 let rec flatten_app mexpr l = match mexpr with
@@ -156,7 +175,7 @@ let rec print_modtype env mp locals mty =
       let seb1 = Option.default mtb1.typ_expr mtb1.typ_expr_alg in
       let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals
       in
-      (try Declaremods.process_module_seb_binding mbid seb1 with _ -> ());
+      nametab_register_module_param mbid seb1;
       hov 2 (str "Funsig" ++ spc () ++ str "(" ++
 	       pr_id (id_of_mbid mbid) ++ str ":" ++
 	       print_modtype env mp1 locals seb1 ++
@@ -164,6 +183,7 @@ let rec print_modtype env mp locals mty =
   | SEBstruct (sign) ->
       let env' = Option.map
 	(Modops.add_signature mp sign Mod_subst.empty_delta_resolver) env in
+      nametab_register_module_body mp sign;
       hv 2 (str "Sig" ++ spc () ++ print_struct false env' mp sign ++
 	    brk (1,-2) ++ str "End")
   | SEBapply _ ->
@@ -190,13 +210,14 @@ let rec print_modexpr env mp locals mexpr = match mexpr with
 	(Modops.add_module (Modops.module_body_of_type mp' mty)) env in
       let typ = Option.default mty.typ_expr mty.typ_expr_alg in
       let locals' = (mbid, get_new_id locals (id_of_mbid mbid))::locals in
-      (try Declaremods.process_module_seb_binding mbid typ with _ -> ());
+      nametab_register_module_param mbid typ;
       hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(id_of_mbid mbid) ++
 	     str ":" ++ print_modtype env mp' locals typ ++
       str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
   | SEBstruct struc ->
       let env' = Option.map
 	(Modops.add_signature mp struc Mod_subst.empty_delta_resolver) env in
+      nametab_register_module_body mp struc;
       hv 2 (str "Struct" ++ spc () ++ print_struct true env' mp struc ++
 	    brk (1,-2) ++ str "End")
   | SEBapply _ ->
@@ -243,7 +264,7 @@ let print_module with_body mp =
   try
     if !short then raise ShortPrinting;
     print_module' (Some (Global.env ())) mp with_body me ++ fnl ()
-  with _ ->
+  with e when Errors.noncritical e ->
     print_module' None mp with_body me ++ fnl ()
 
 let print_modtype kn =
@@ -254,5 +275,5 @@ let print_modtype kn =
      (try
 	if !short then raise ShortPrinting;
 	print_modtype' (Some (Global.env ())) kn mtb.typ_expr
-      with _ ->
+      with e when Errors.noncritical e ->
 	print_modtype' None kn mtb.typ_expr))
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index dbc06856..77364180 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -188,11 +188,11 @@ let declare_tactic loc s cl =
                  Tacexpr.TacExtend($default_loc$,$se$,l)))
            | None -> () ])
           $atomic_tactics$
-      with e ->
+      with [ e when Errors.noncritical e ->
 	    Pp.msg_warning
 	      (Stream.iapp
 	        (Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
-	        (Errors.print e));
+	        (Errors.print e)) ];
       Egrammar.extend_tactic_grammar $se$ $gl$;
       List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
     ])
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 4f39019f..bcdf7cff 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -55,11 +55,11 @@ let declare_command loc s nt cl =
   declare_str_items loc
     [ <:str_item< do {
 	try Vernacinterp.vinterp_add $se$ $funcl$
-	with e ->
+	with [ e when Errors.noncritical e ->
 	  Pp.msg_warning
 	    (Stream.iapp
 	       (Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
-	       (Errors.print e));
+	       (Errors.print e)) ];
 	Egrammar.extend_vernac_command_grammar $se$ $nt$ $gl$
       } >> ]
 
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index d0f81dad..1c021eee 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -404,7 +404,8 @@ let rec canonize_name c =
 let build_subst uf subst =
   Array.map (fun i ->
 	       try term uf i
-	       with _ -> anomaly "incomplete matching") subst
+	       with e when Errors.noncritical e ->
+                 anomaly "incomplete matching") subst
 
 let rec inst_pattern subst = function
     PVar i ->
@@ -730,9 +731,7 @@ let __eps__ = id_of_string "_eps_"
 let new_state_var typ state =
   let id = pf_get_new_id __eps__ state.gls in
   let {it=gl ; sigma=sigma} = state.gls in
-  let new_hyps =
-    Environ.push_named_context_val (id,None,typ) (Goal.V82.hyps sigma gl) in
-  let gls = Goal.V82.new_goal_with sigma gl new_hyps in
+  let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in
     state.gls<- gls;
     id
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 95ff4d34..764e36b0 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -129,7 +129,9 @@ let non_trivial = function
 
 let patterns_of_constr env sigma nrels term=
   let f,args=
-    try destApp (whd_delta env term) with _ -> raise Not_found in
+    try destApp (whd_delta env term)
+    with e when Errors.noncritical e -> raise Not_found
+  in
 	if eq_constr f (Lazy.force _eq) && (Array.length args)=3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 730051c1..da88d48d 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -75,9 +75,9 @@ let mode_of_pftreestate pts =
       Mode_proof
 	  
 let get_current_mode () =
-  try 
+  try
     mode_of_pftreestate (Pfedit.get_pftreestate ())
-  with _ -> Mode_none
+  with e when Errors.noncritical e -> Mode_none
 
 let check_not_proof_mode str =
  if get_current_mode () = Mode_proof then
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 72caeaed..ab161b35 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -381,7 +381,7 @@ let find_subsubgoal c ctyp skip submetas gls =
 		  se.se_meta submetas se.se_meta_list}
 	  else
 	      dfs (pred n)
-      with _ ->
+      with e when Errors.noncritical e ->
 	begin
 	  enstack_subsubgoals env se stack gls;
 	  dfs n
@@ -519,7 +519,10 @@ let decompose_eq id gls =
 
 let instr_rew _thus rew_side cut gls0 =
   let last_id =
-    try get_last (pf_env gls0) with _ -> error "No previous equality." in
+    try get_last (pf_env gls0)
+    with e when Errors.noncritical e ->
+      error "No previous equality."
+  in
   let typ,lhs,rhs = decompose_eq last_id gls0 in
   let items_tac gls =
     match cut.cut_by with
@@ -849,7 +852,7 @@ let build_per_info etype casee gls =
   let ind =
     try
       destInd hd
-    with _ ->
+    with e when Errors.noncritical e ->
       error "Case analysis must be done on an inductive object." in
   let mind,oind = Global.lookup_inductive ind in
   let nparams,index =
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 6aa47eff..b7ee3c1a 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -397,8 +397,10 @@ let mono_filename f =
 	in
 	let id =
 	  if lang () <> Haskell then default_id
-	  else try id_of_string (Filename.basename f)
-	  with _ -> error "Extraction: provided filename is not a valid identifier"
+	  else
+            try id_of_string (Filename.basename f)
+	    with e when Errors.noncritical e ->
+              error "Extraction: provided filename is not a valid identifier"
 	in
 	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
 
@@ -473,8 +475,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
     msg_with ft (d.preamble mo opened unsafe_needs);
     msg_with ft (d.pp_struct struc);
     Option.iter close_out cout;
-  with e ->
-    Option.iter close_out cout; raise e
+  with reraise ->
+    Option.iter close_out cout; raise reraise
   end;
   if not dry then Option.iter info_file fn;
   (* Now, let's print the signature *)
@@ -487,8 +489,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
 	 msg_with ft (d.sig_preamble mo opened unsafe_needs);
 	 msg_with ft (d.pp_sig (signature_of_structure struc));
 	 close_out cout;
-       with e ->
-	 close_out cout; raise e
+       with reraise ->
+	 close_out cout; raise reraise
        end;
        info_file si)
     (if dry then None else si);
@@ -527,7 +529,9 @@ let rec locate_ref = function
   | r::l ->
       let q = snd (qualid_of_reference r) in
       let mpo = try Some (Nametab.locate_module q) with Not_found -> None
-      and ro = try Some (Smartlocate.global_with_alias r) with _ -> None
+      and ro =
+        try Some (Smartlocate.global_with_alias r)
+        with e when Errors.noncritical e -> None
       in
       match mpo, ro with
 	| None, None -> Nametab.error_global_not_found q
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0a17453c..e5357336 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -149,7 +149,7 @@ let rec handle_exn r n fn_name = function
 	 (fun i ->
 	    assert ((0 < i) && (i <= n));
 	    MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
-       with _ -> MLexn s)
+       with e when Errors.noncritical e -> MLexn s)
   | a -> ast_map (handle_exn r n fn_name) a
 
 (*S Management of type variable contexts. *)
@@ -683,7 +683,7 @@ and extract_cst_app env mle mlt kn args =
 	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
 	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
-      with _ -> mla
+      with e when Errors.noncritical e -> mla
   in
   (* For strict languages, purely logical signatures with at least
      one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 6c78b533..b6fc5ac8 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -81,7 +81,9 @@ let kn_sig =
 let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ -> assert false
-    | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
+    | Tvar i ->
+      (try pr_id (List.nth vl (pred i))
+       with e when Errors.noncritical e -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
     | Tglob (IndRef(kn,0),l)
 	when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index a38b303f..d0bf387a 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -879,7 +879,7 @@ let is_program_branch = function
     (try
        ignore (int_of_string (String.sub s n (String.length s - n)));
        String.sub s 0 n = br
-     with _ -> false)
+     with e when Errors.noncritical e -> false)
   | Tmp _ | Dummy -> false
 
 let expand_linear_let o id e =
@@ -1312,7 +1312,7 @@ let inline_test r t =
     let c = match r with ConstRef c -> c | _ -> assert false in
     let has_body =
       try constant_has_body (Global.lookup_constant c)
-      with _ -> false
+      with e when Errors.noncritical e -> false
     in
     has_body &&
       (let t1 = eta_red t in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 289b2a1d..4e8d8145 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -119,7 +119,8 @@ let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ | Taxiom -> assert false
     | Tvar i -> (try pp_tvar (List.nth vl (pred i))
-		 with _ -> (str "'a" ++ int i))
+		 with e when Errors.noncritical e ->
+                   (str "'a" ++ int i))
     | Tglob (r,[a1;a2]) when is_infix r ->
 	pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
     | Tglob (r,[]) -> pp_global Type r
@@ -188,7 +189,7 @@ let rec pp_expr par env args =
 	   let args = list_skipn (projection_arity r) args in
 	   let record = List.hd args in
 	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
-	 with _ -> apply (pp_global Term r))
+	 with e when Errors.noncritical e -> apply (pp_global Term r))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
 	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index e0a6e843..497ddf03 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -255,7 +255,7 @@ let safe_basename_of_global r =
 
 let string_of_global r =
  try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
- with _ -> string_of_id (safe_basename_of_global r)
+ with e when Errors.noncritical e -> string_of_id (safe_basename_of_global r)
 
 let safe_pr_global r = str (string_of_global r)
 
@@ -263,7 +263,7 @@ let safe_pr_global r = str (string_of_global r)
 
 let safe_pr_long_global r =
   try Printer.pr_global r
-  with _ -> match r with
+  with e when Errors.noncritical e -> match r with
     | ConstRef kn ->
 	let mp,_,l = repr_con kn in
 	str ((string_of_mp mp)^"."^(string_of_label l))
@@ -452,7 +452,7 @@ let my_bool_option name initval =
 
 (*s Extraction AccessOpaque *)
 
-let access_opaque = my_bool_option "AccessOpaque" false
+let access_opaque = my_bool_option "AccessOpaque" true
 
 (*s Extraction AutoInline *)
 
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 9d3d8c99..29d41b81 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -85,7 +85,7 @@ let gen_ground_tac flag taco ids bases gl=
 	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
       let result=ground_tac solver startseq gl in
 	qflag:=backup;result
-    with e ->qflag:=backup;raise e
+    with reraise ->qflag:=backup;raise reraise
 
 (* special for compatibility with Intuition
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 68f112d6..4b07c609 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -129,7 +129,7 @@ let mk_open_instance id gl m t=
 	| _-> anomaly "can't happen" in
   let ntt=try
     Pretyping.Default.understand evmap env (raux m rawt)
-  with _ ->
+  with e when Errors.noncritical e ->
     error "Untypable instance, maybe higher-order non-prenex quantification" in
     decompose_lam_n_assum m ntt
 
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index 043c9e51..1574e21e 100644
--- a/plugins/fourier/fourier.ml
+++ b/plugins/fourier/fourier.ml
@@ -175,7 +175,7 @@ let unsolvable lie =
 			raise (Failure "contradiction found"))
           |_->assert false)
 			     lr)
-   with _ -> ());
+   with e when Errors.noncritical e -> ());
    !res
 ;;
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index cdd10d70..e0e4f7d6 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -40,7 +40,7 @@ type flin = {fhom: rational Constrhash.t;
 
 let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};;
 
-let flin_coef f x = try (Constrhash.find f.fhom x) with _-> r0;;
+let flin_coef f x = try (Constrhash.find f.fhom x) with Not_found -> r0;;
 
 let flin_add f x c =
     let cx = flin_coef f x in
@@ -141,10 +141,12 @@ let rec flin_of_constr c =
 	     (try (let a=(rational_of_constr args.(0)) in
                      try (let b = (rational_of_constr args.(1)) in
 			    (flin_add_cste (flin_zero()) (rmult a b)))
-		     with _-> (flin_add (flin_zero())
+		     with e when Errors.noncritical e ->
+                       (flin_add (flin_zero())
 				 args.(1)
 				 a))
-	      with _-> (flin_add (flin_zero())
+	      with e when Errors.noncritical e ->
+                (flin_add (flin_zero())
 			  args.(0)
 			  (rational_of_constr args.(1))))
 	 | "Rinv"->
@@ -154,7 +156,8 @@ let rec flin_of_constr c =
 	     (let b=(rational_of_constr args.(1)) in
 		try (let a = (rational_of_constr args.(0)) in
 		       (flin_add_cste (flin_zero()) (rdiv a b)))
-		with _-> (flin_add (flin_zero())
+		with e when Errors.noncritical e ->
+                  (flin_add (flin_zero())
 		            args.(0)
                             (rinv b)))
          |_->assert false)
@@ -164,7 +167,8 @@ let rec flin_of_constr c =
               |"R0" -> flin_zero ()
               |_-> assert false)
   |_-> assert false)
-  with _ -> flin_add (flin_zero())
+  with e when Errors.noncritical e ->
+    flin_add (flin_zero())
                      c
 	             r1
 ;;
@@ -494,13 +498,13 @@ let rec fourier gl=
 	    |_->assert false)
         |_->assert false
       in tac gl)
-     with _ ->
+     with e when Errors.noncritical e ->
     (* les hypothèses *)
     let hyps = List.map (fun (h,t)-> (mkVar h,t))
                         (list_of_sign (pf_hyps gl)) in
     let lineq =ref [] in
     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
-		        with _ -> ())
+		        with e when Errors.noncritical e -> ())
               hyps;
     (* lineq = les inéquations découlant des hypothèses *)
     if !lineq=[] then Util.error "No inequalities";
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 33d77568..48205019 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -33,9 +33,12 @@ let observennl strm =
 
 let do_observe_tac s tac g =
  try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
- with e ->
-   let e = Cerrors.process_vernac_interp_error e in
-   let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
+ with reraise ->
+   let e = Cerrors.process_vernac_interp_error reraise in
+   let goal =
+     try (Printer.pr_goal g)
+     with e when Errors.noncritical e -> assert false
+   in
    msgnl (str "observation "++ s++str " raised exception " ++
 	    Errors.print e ++ str " on goal " ++ goal );
    raise e;;
@@ -119,7 +122,7 @@ let is_trivial_eq t =
 	    eq_constr t1 t2 && eq_constr a1 a2
 	| _ -> false
     end
-  with _ -> false
+  with e when Errors.noncritical e -> false
   in
 (*   observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
   res
@@ -145,7 +148,7 @@ let is_incompatible_eq t =
 	    (eq_constr u1 u2 &&
 	       incompatible_constructor_terms t1 t2)
 	| _ -> false
-    with _ -> false
+    with e when Errors.noncritical e -> false
   in
   if res then   observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t);
   res
@@ -232,7 +235,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	  then
 	    (jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0))
 	  else nochange "not an equality"
-      with _ -> nochange "not an equality"
+      with e when Errors.noncritical e -> nochange "not an equality"
     in
     if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs";
     let rec compute_substitution sub t1 t2 =
@@ -608,7 +611,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 let my_orelse tac1 tac2 g =
   try
     tac1 g
-  with e ->
+  with e when Errors.noncritical e ->
 (*     observe (str "using snd tac since : " ++ Errors.print e); *)
     tac2 g
 
@@ -1212,7 +1215,11 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	let ctxt,pte_app =  (decompose_prod_assum (pf_concl gl)) in
 	let pte,pte_args = (decompose_app pte_app) in
 	try
-	  let pte = try destVar pte with _ -> anomaly "Property is not a variable"  in
+	  let pte =
+            try destVar pte
+            with e when Errors.noncritical e ->
+              anomaly "Property is not a variable"
+          in
 	  let fix_info = Idmap.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 00e966fb..04fcc8d4 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -302,11 +302,8 @@ let defined () =
 	  "defined"
 	  ((try
 	      str "On goal : " ++ fnl () ++  pr_open_subgoals () ++ fnl ()
-	    with _ -> mt ()
+	    with e when Errors.noncritical e -> mt ()
 	   ) ++msg)
-    | e -> raise e
-
-
 
 let build_functional_principle interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
@@ -401,7 +398,7 @@ let generate_functional_principle
      Don't forget to close the goal if an error is raised !!!!
   *)
   save false new_princ_name entry g_kind hook
-  with e ->
+  with e when Errors.noncritical e ->
     begin
       begin
 	try
@@ -413,7 +410,7 @@ let generate_functional_principle
 	  then Pfedit.delete_current_proof ()
 	  else ()
 	  else ()
-	with _ -> ()
+	with e when Errors.noncritical e -> ()
       end;
       raise (Defining_principle e)
     end
@@ -554,7 +551,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition
 	0
 	(prove_princ_for_struct false 0 (Array.of_list funs))
 	(fun _ _ _ -> ())
-  with e ->
+  with e when Errors.noncritical e ->
     begin
       begin
 	try
@@ -566,7 +563,7 @@ let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition
 	  then Pfedit.delete_current_proof ()
 	  else ()
 	  else ()
-	with _ -> ()
+	with e when Errors.noncritical e -> ()
       end;
       raise (Defining_principle e)
     end
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 85d79214..6b6e4838 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -208,14 +208,14 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
 		    try Functional_principles_types.build_scheme fas
 		    with Functional_principles_types.No_graph_found ->
 		      Util.error ("Cannot generate induction principle(s)")
-    		      | e ->
+    		      | e when Errors.noncritical e ->
 			  let names = List.map (fun (_,na,_) -> na) fas in
 			  warning_error names e
 
 		  end
 	      | _ -> assert false (* we can only have non empty  list *)
 	  end
-	  | e -> 
+	  | e when Errors.noncritical e ->
 	      let names = List.map (fun (_,na,_) -> na) fas in
 	      warning_error names e
       end
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 43b08840..b9e0e62a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -948,7 +948,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  try
 		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
 		    let t' =
-		      try Pretyping.Default.understand Evd.empty env t with _ -> raise Continue
+		      try Pretyping.Default.understand Evd.empty env t
+                      with e when Errors.noncritical e -> raise Continue
 		    in
 		    let is_in_b = is_free_in id b in
 		    let _keep_eq =
@@ -1247,7 +1248,7 @@ let compute_params_name relnames (args : (Names.name * Glob_term.glob_constr * b
 	     l := param::!l
 	)
 	rels_params.(0)
-    with _ ->
+    with e when Errors.noncritical e ->
       ()
   in
   List.rev !l
@@ -1453,7 +1454,7 @@ let do_build_inductive
 	in
 	observe (msg);
 	raise e
-    | e ->
+    | reraise ->
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let repacked_rel_inds =
@@ -1464,16 +1465,16 @@ let do_build_inductive
 	  str "while trying to define"++ spc () ++
 	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
 	    ++ fnl () ++
-	    Errors.print e
+	    Errors.print reraise
 	in
  	observe msg;
-	raise e
+	raise reraise
 
 
 
 let build_inductive funnames funsargs returned_types rtl =
   try
     do_build_inductive funnames funsargs returned_types rtl
-  with e -> raise (Building_graph e)
+  with e when Errors.noncritical e -> raise (Building_graph e)
 
 
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index cdd0eaf7..6cc932b1 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -534,7 +534,8 @@ let rec are_unifiable_aux  = function
 	     else
 	       let eqs' =
  		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly "are_unifiable_aux"
+		 with e when Errors.noncritical e ->
+                   anomaly "are_unifiable_aux"
 	       in
 	       are_unifiable_aux eqs'
 
@@ -556,7 +557,8 @@ let rec eq_cases_pattern_aux  = function
 	     else
 	       let eqs' =
  		 try  ((List.combine cpl1 cpl2)@eqs)
-		 with _ -> anomaly "eq_cases_pattern_aux"
+		 with e when Errors.noncritical e ->
+                   anomaly "eq_cases_pattern_aux"
 	       in
 	       eq_cases_pattern_aux eqs'
 	 | _ -> raise NotUnifiable
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 8caeca57..d2c065a0 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -82,7 +82,7 @@ let functional_induction with_clean c princl pat =
       List.fold_right
 	(fun a acc ->
 	  try Idset.add (destVar a) acc
-	  with _ -> acc
+	  with e when Errors.noncritical e -> acc
 	)
 	args
 	Idset.empty
@@ -166,8 +166,8 @@ let build_newrecursive
 	       sigma rec_sign rec_impls def
 	  )
           lnameargsardef
-	with e ->
-	States.unfreeze fs; raise e in
+	with reraise ->
+	States.unfreeze fs; raise reraise in
     States.unfreeze fs; def
   in
   recdef,rec_impls
@@ -251,12 +251,12 @@ let derive_inversion fix_names =
 	   (fun id -> destInd (Constrintern.global_reference (mk_rel_id id)))
 	   fix_names
 	)
-    with e ->
+    with e when Errors.noncritical e ->
       let e' = Cerrors.process_vernac_interp_error e in
       msg_warning
 	(str "Cannot build inversion information" ++
 	   if do_observe () then (fnl() ++ Errors.print e') else mt ())
-  with _ -> ()
+  with e when Errors.noncritical e -> ()
 
 let warning_error names e =
   let e = Cerrors.process_vernac_interp_error e in
@@ -346,7 +346,7 @@ let generate_principle  on_error
 	Array.iter (add_Function is_general) funs_kn;
 	()
       end
-  with e ->
+  with e when Errors.noncritical e ->
     on_error names e
 
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
@@ -413,7 +413,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	   functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
 	);
       derive_inversion [fname]
-    with e ->
+    with e when Errors.noncritical e ->
       (* No proof done *)
       ()
   in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index dd475315..827191b1 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -55,7 +55,6 @@ let locate_with_msg msg f x =
     f x
   with
     | Not_found -> raise (Util.UserError("", msg))
-    | e -> raise e
 
 
 let filter_map filter f =
@@ -123,7 +122,7 @@ let def_of_const t =
       (try (match Declarations.body_of_constant (Global.lookup_constant sp) with
              | Some c -> Declarations.force c
 	     | _ -> assert false)
-       with _ -> assert false)
+       with e when Errors.noncritical e -> assert false)
     |_ -> assert false
 
 let coq_constant s =
@@ -215,13 +214,13 @@ let with_full_print f a =
     Dumpglob.continue ();
     res
   with
-    | e ->
+    | reraise ->
 	Impargs.make_implicit_args old_implicit_args;
 	Impargs.make_strict_implicit_args old_strict_implicit_args;
 	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
 	Flags.raw_print := old_rawprint;
 	Dumpglob.continue ();
-	raise e
+	raise reraise
 
 
 
@@ -350,7 +349,8 @@ open Term
 let pr_info f_info =
   str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
     str "function_constant_type := " ++
-    (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
+    (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant))
+     with e when Errors.noncritical e -> mt ()) ++ fnl () ++
     str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
     str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
     str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
@@ -502,22 +502,22 @@ exception ToShow of exn
 let init_constant dir s =
   try
     Coqlib.gen_constant "Function" dir s
-  with e -> raise (ToShow e)
+  with e when Errors.noncritical e -> raise (ToShow e)
 
 let jmeq () =
   try
     (Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
      init_constant ["Logic";"JMeq"] "JMeq")
-  with e -> raise (ToShow e)
+  with e when Errors.noncritical e -> raise (ToShow e)
 
 let jmeq_rec () =
   try
     Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
 	  init_constant ["Logic";"JMeq"] "JMeq_rec"
-  with e -> raise (ToShow e)
+  with e when Errors.noncritical e -> raise (ToShow e)
 
 let jmeq_refl () =
   try
     Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
     init_constant ["Logic";"JMeq"] "JMeq_refl"
-  with e -> raise (ToShow e)
+  with e when Errors.noncritical e -> raise (ToShow e)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 55451a9f..7b5dd763 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -59,14 +59,17 @@ let observennl strm =
 
 
 let do_observe_tac s tac g =
-  let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
+  let goal =
+    try Printer.pr_goal g
+    with e when Errors.noncritical e -> assert false
+  in
   try
     let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
-  with e ->
-    let e' = Cerrors.process_vernac_interp_error e in
+  with reraise ->
+    let e' = Cerrors.process_vernac_interp_error reraise in
     msgnl (str "observation "++ s++str " raised exception " ++
 	     Errors.print e' ++ str " on goal " ++ goal );
-    raise e;;
+    raise reraise;;
 
 
 let observe_tac s tac g =
@@ -568,7 +571,7 @@ let rec reflexivity_with_destruct_cases g =
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
 	| _ -> reflexivity
-    with _ -> reflexivity
+    with e when Errors.noncritical e -> reflexivity
   in
   let eq_ind =     Coqlib.build_coq_eq () in
   let discr_inject =
@@ -862,11 +865,11 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs;
-  with e ->
+  with reraise ->
     (* In case of problem, we reset all the lemmas *)
     Pfedit.delete_all_proofs ();
     States.unfreeze previous_state;
-    raise e
+    raise reraise
 
 
 
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 6ee2f352..bd1a1710 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -70,7 +70,7 @@ let ident_global_exist id =
     let ans = CRef (Libnames.Ident (dummy_loc,id)) in
     let _ = ignore (Constrintern.intern_constr Evd.empty (Global.env()) ans) in
     true
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 (** [next_ident_fresh id] returns a fresh identifier (ie not linked in
     global env) with base [id]. *)
@@ -793,10 +793,10 @@ let rec merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
 
   let params1 =
     try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
-    with _ -> [] in
+    with e when Errors.noncritical e -> [] in
   let params2 =
     try fst (glob_decompose_prod_n shift.nrecprms2 (List.hd lcstr2))
-    with _ -> [] in
+    with e when Errors.noncritical e -> [] in
 
   let lcstr1 = List.combine (Array.to_list oib1.mind_consnames) lcstr1 in
   let lcstr2 = List.combine (Array.to_list oib2.mind_consnames) lcstr2 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 892c1a77..9853fd73 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -94,11 +94,11 @@ let do_observe_tac s tac g =
     let v = tac g in 
     ignore(Stack.pop debug_queue);
     v
-  with e -> 
+  with reraise ->
     if not (Stack.is_empty debug_queue)
     then
-      print_debug_queue true e;
-    raise e
+      print_debug_queue true reraise;
+    raise reraise
 
 let observe_tac s tac g =
   if Tacinterp.get_debug () <> Tactic_debug.DebugOff
@@ -140,7 +140,7 @@ let def_of_const t =
       (try (match body_of_constant (Global.lookup_constant sp) with
              | Some c -> Declarations.force c
 	     | _ -> assert false)
-       with _ ->
+       with e when Errors.noncritical e ->
 	 anomaly ("Cannot find definition of constant "^
 		    (string_of_id (id_of_label (con_label sp))))
       )
@@ -380,7 +380,11 @@ let rec  mk_intros_and_continue thin_intros (extra_eqn:bool)
 		(fun g1 ->
 		   let ty_teq = pf_type_of g1 (mkVar teq) in
 		   let teq_lhs,teq_rhs =
-		     let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
+		     let _,args =
+                       try destApp ty_teq
+                       with e when Errors.noncritical e ->
+                         Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false
+                     in
 		     args.(1),args.(2)
 		   in
 	           cont_function (mkVar teq::eqs) (Termops.replace_term teq_lhs teq_rhs expr) g1
@@ -701,12 +705,17 @@ let proveterminate nb_arg rec_arg_id is_mes acc_inv (hrec:identifier)
             (match find_call_occs  nb_arg 0 f_constr expr with
 	      _,[] ->
 	      (try observe_tac "base_leaf" (base_leaf func eqs expr)
-	       with e -> (msgerrnl (str "failure in base case");raise e ))
+	       with reraise ->
+                 (msgerrnl (str "failure in base case");raise reraise ))
 	    | _, _::_ ->
 	      observe_tac "rec_leaf"
 	        (rec_leaf is_mes acc_inv hrec func eqs expr)) in
       v
-    with e -> begin msgerrnl(str "failure in proveterminate"); raise e end
+    with reraise ->
+      begin
+        msgerrnl(str "failure in proveterminate");
+        raise reraise
+      end
   in
   proveterminate
 
@@ -931,7 +940,7 @@ let is_rec_res id =
   let id_name = string_of_id id in
   try
     String.sub id_name 0 (String.length rec_res_name) = rec_res_name
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 let clear_goals =
   let rec clear_goal t =
@@ -969,7 +978,8 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     | Some s -> s
     | None   ->
 	try (add_suffix current_proof_name "_subproof")
-	with _ -> anomaly "open_new_goal with an unamed theorem"
+	with e when Errors.noncritical e ->
+          anomaly "open_new_goal with an unamed theorem"
   in
   let sign = initialize_named_context_for_proof () in
   let na = next_global_ident_away name [] in
@@ -1439,7 +1449,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
     let stop = ref false in
     begin
       try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type)
-      with e ->
+      with e when Errors.noncritical e ->
 	begin
 	  if Tacinterp.get_debug () <> Tactic_debug.DebugOff
 	  then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
@@ -1474,9 +1484,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       using_lemmas
       (List.length res_vars)
       hook
-  with e ->
+  with reraise ->
     begin
-      (try ignore (Backtrack.backto previous_label) with _ -> ());
+      (try ignore (Backtrack.backto previous_label)
+       with e when Errors.noncritical e -> ());
       (*       anomaly "Cannot create termination Lemma" *)
-      raise e
+      raise reraise
     end
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 25579a87..a5b0da9c 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -331,7 +331,7 @@ let dual_raw_certificate (l:  (Poly.t * Mc.op1) list) =
     | Inr _ -> None
     | Inl cert ->  Some (rats_to_ints (Vect.to_list cert)) 
        (* should not use rats_to_ints *)
-  with x -> 
+  with x when Errors.noncritical x ->
    if debug 
    then (Printf.printf "raw certificate %s" (Printexc.to_string x);   
          flush stdout) ;
@@ -377,8 +377,9 @@ let linear_prover n_spec l  =
 
 
 let linear_prover n_spec l  =
- try linear_prover n_spec l with
-   x -> (print_string (Printexc.to_string x); None)
+ try linear_prover n_spec l
+ with x when x <> Sys.Break ->
+   (print_string (Printexc.to_string x); None)
 
 let linear_prover_with_cert spec l = 
   match linear_prover spec l with
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 2020447f..ff08aeb3 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -937,7 +937,8 @@ struct
                            let (expr,env) = parse_expr env args.(0) in
                            let power = (parse_exp expr args.(1)) in
                              (power  , env)
-			 with _ ->   (* if the exponent is a variable *)
+			 with e when e <> Sys.Break ->
+                           (* if the exponent is a variable *)
                            let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
                        end
                    | Ukn  s ->
@@ -1112,8 +1113,12 @@ struct
   
   let parse_formula parse_atom env tg term =
 
-    let parse_atom env tg t = try let (at,env) = parse_atom env t in
-                                    (A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in
+    let parse_atom env tg t =
+      try
+        let (at,env) = parse_atom env t in
+        (A(at,tg,t), env,Tag.next tg)
+      with e when e <> Sys.Break -> (X(t),env,tg)
+    in
 
     let rec xparse_formula env tg term =
      match kind_of_term term with
@@ -1189,7 +1194,8 @@ let same_proof sg cl1 cl2 =
  let rec xsame_proof sg =
   match sg with
    | [] -> true
-   | n::sg -> (try List.nth cl1 n = List.nth cl2 n with _ -> false)
+   | n::sg ->
+     (try List.nth cl1 n = List.nth cl2 n with e when e <> Sys.Break -> false)
       && (xsame_proof sg ) in
   xsame_proof sg
 
@@ -1253,7 +1259,7 @@ let btree_of_array typ a  =
 let btree_of_array typ a =
  try
   btree_of_array typ a
- with x ->
+ with x when x <> Sys.Break ->
   failwith (Printf.sprintf "btree of array : %s" (Printexc.to_string x))
 
 let dump_varmap typ env =
@@ -1322,7 +1328,7 @@ let rec parse_hyps parse_arith env tg hyps =
       try
        let (c,env,tg) = parse_formula parse_arith env  tg t in
 	((i,c)::lhyps, env,tg)
-      with _ -> 		(lhyps,env,tg)
+      with e when e <> Sys.Break -> 		(lhyps,env,tg)
        (*(if debug then Printf.printf "parse_arith : %s\n" x);*)
 
 
@@ -1466,7 +1472,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
           (pp_ml_list prover.pp_f) (List.map fst new_cl)   ;
           flush stdout
       end ; *)
-    let res = try prover.compact prf remap with x ->
+    let res = try prover.compact prf remap with x when x <> Sys.Break ->
       if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
       (* This should not happen -- this is the recovery plan... *)
       match prover.prover (List.map fst new_cl) with
@@ -2031,13 +2037,13 @@ let xlia gl =
   try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
       [ linear_Z ] gl
-  with z -> (*Printexc.print_backtrace stdout ;*) raise z
+  with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
 let xnlia gl =
   try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
       [ nlinear_Z ] gl
-  with z -> (*Printexc.print_backtrace stdout ;*) raise z
+  with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
 
 
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index dfda5984..0f26575c 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -150,7 +150,7 @@ let real_nonlinear_prover d l =
    S (Some proof)
  with
   | Sos_lib.TooDeep -> S None
-  |    x        ->   F (Printexc.to_string x)
+  | x when x <> Sys.Break -> F (Printexc.to_string x)
 
 (* This is somewhat buggy, over Z, strict inequality vanish... *)
 let pure_sos  l =
@@ -174,7 +174,7 @@ let pure_sos  l =
     S (Some proof)
  with
 (*   | Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *)
-   |  x        -> (* May be that could be refined *) S None
+   | x when x <> Sys.Break -> (* May be that could be refined *) S None
 
 
 
@@ -203,7 +203,7 @@ let main () =
       Marshal.to_channel  chan (cert:csdp_certificate) [] ;
       flush chan ;
       exit 0
-  with  x -> (Printf.fprintf chan "error %s" (Printexc.to_string x)  ; exit 1)
+  with any -> (Printf.fprintf chan "error %s" (Printexc.to_string any)  ; exit 1)
 
 ;;
 
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index d9201722..6effa4c4 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -728,7 +728,8 @@ struct
 	    try
 	      Some (bound_of_variable IMap.empty fresh s.sys)
 	    with
-		x -> Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None
+	      x when x <> Sys.Break ->
+                Printf.printf "optimise Exception : %s" (Printexc.to_string x) ; None
 
 
   let find_point cstrs =
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index ccbf0406..3129e54d 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -29,10 +29,10 @@ let finally f rst =
   try
     let res = f () in
       rst () ; res
-  with x ->
+  with reraise ->
     (try rst ()
-    with _  -> raise x
-    ); raise x
+    with any  -> raise reraise
+    ); raise reraise
 
 let map_option f x =
   match x with
@@ -431,14 +431,16 @@ let command exe_path args vl =
 	    | Unix.WEXITED 0 ->
 		let inch  = Unix.in_channel_of_descr stdout_read in
 		  begin try Marshal.from_channel inch 
-                        with x -> failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x)) 
+                        with x when x <> Sys.Break ->
+                          failwith (Printf.sprintf "command \"%s\" exited %s" exe_path (Printexc.to_string x))
                   end
 	    | Unix.WEXITED i   -> failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
 	    | Unix.WSIGNALED i -> failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i)
 	    | Unix.WSTOPPED i  -> failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i))
         (* Cleanup  *)
 	(fun () ->
-	  List.iter (fun x -> try Unix.close x with _ -> ()) [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write])
+	  List.iter (fun x -> try Unix.close x with e when e <> Sys.Break -> ())
+            [stdin_read; stdin_write; stdout_read; stdout_write; stderr_read; stderr_write])
 
 (* Local Variables: *)
 (* coding: utf-8 *)
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index cb7a9280..6d1a2927 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -82,10 +82,10 @@ let finally f rst =
   try
     let res = f () in
       rst () ; res
-  with x ->
+  with reraise ->
     (try rst ()
-    with _  -> raise x
-    ); raise x
+    with any  -> raise reraise
+    ); raise reraise
 
 
 let read_key_elem inch =
@@ -93,7 +93,7 @@ let read_key_elem inch =
     Some (Marshal.from_channel inch)
   with
     | End_of_file -> None
-    |    _        -> raise InvalidTableFormat
+    | e when e <> Sys.Break -> raise InvalidTableFormat
 
 (** In win32, it seems that we should unlock the exact zone
     that has been locked, and not the whole file *)
@@ -151,7 +151,7 @@ let open_in f =
 	    Table.iter 
 	      (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
 	    flush outch ; 
-	  with  _ -> () )
+	  with e when e <> Sys.Break -> () )
 	    ;
 	    unlock out ; 
 	    { outch = outch ;
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 996dbadd..68fb2626 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -237,7 +237,8 @@ open Format
 
 let getvar lv i =
   try (nth lv i)
-  with _ -> (fold_left (fun r x -> r^" "^x) "lv= " lv)
+  with e when Errors.noncritical e ->
+    (fold_left (fun r x -> r^" "^x) "lv= " lv)
     ^" i="^(string_of_int i)
 
 let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
@@ -590,7 +591,7 @@ let coefpoldep = Hashtbl.create 51
 (* coef of q in p = sum_i c_i*q_i *)
 let coefpoldep_find p q =
   try (Hashtbl.find coefpoldep (p.num,q.num))
-  with _ -> []
+  with Not_found -> []
 
 let coefpoldep_remove p q =
   Hashtbl.remove coefpoldep (p.num,q.num)
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index 0eea961d..fdc8e865 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -173,7 +173,7 @@ let rec equal p q =
 			       then failwith "raté")
 		    p1;
 		  true)
-	     with _ -> false)
+	     with e when Errors.noncritical e -> false)
     | (_,_) -> false
 
 (* normalize polynomial: remove head zeros, coefficients are normalized
@@ -524,7 +524,7 @@ let div_pol_rat p q=
 		   q x in
          (* degueulasse, mais c 'est pour enlever un warning *)
          if s==s then true else true)
-    with _ -> false
+    with e when Errors.noncritical e -> false
 
 (***********************************************************************
   5. Pseudo-division and gcd with subresultants.
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index c16bd425..17c8654b 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -33,10 +33,11 @@ let set_of_list_eq eq l =
 
 let memos s memoire nf f x =
    try (let v = Hashtbl.find memoire (nf x) in pr s;v)
-   with _ -> (pr "#";
-	      let v = f x in
-	      Hashtbl.add memoire (nf x) v;
-	      v)
+   with e when Errors.noncritical e ->
+     (pr "#";
+      let v = f x in
+      Hashtbl.add memoire (nf x) v;
+      v)
 
 
 (**********************************************************************
@@ -64,7 +65,7 @@ let facteurs_liste div constant lp =
                                    if not (constant r)
 				   then l1:=r::(!l1)
                                    else p_dans_lmin:=true)
-			      with _ -> ())
+			      with e when Errors.noncritical e -> ())
                      lmin;
           if !p_dans_lmin
           then factor lmin lp1
@@ -75,7 +76,8 @@ let facteurs_liste div constant lp =
                 List.iter (fun q -> try (let r = div q p in
 					 if not (constant r)
 					 then l1:=r::(!l1))
-				    with _ -> lmin1:=q::(!lmin1))
+				    with e when Errors.noncritical e ->
+                                      lmin1:=q::(!lmin1))
                           lmin;
 	        factor (List.rev (p::(!lmin1))) !l1)
           (* au moins un q de lmin divise p non trivialement *)
@@ -105,7 +107,7 @@ let factorise_tableau div zero c f l1 =
       	                       li:=j::(!li);
                                r:=rr;
 			   done)
-                      with _ -> ())
+                      with e when Errors.noncritical e -> ())
                   l1;
       res.(i)<-(!r,!li))
      f;
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 028ef95d..ffa99fc7 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -885,7 +885,7 @@ let rec transform p t =
     try
       let v,th,_ = find_constr t' in
       [clever_rewrite_base p (mkVar v) (mkVar th)], Oatom v
-    with _ ->
+    with e when Errors.noncritical e ->
       let v = new_identifier_var ()
       and th = new_identifier () in
       hide_constr t' v th isnat;
@@ -924,7 +924,8 @@ let rec transform p t =
          | _ -> default false t
        end
    | Kapp((Zpos|Zneg|Z0),_) ->
-       (try ([],Oz(recognize_number t)) with _ -> default false t)
+       (try ([],Oz(recognize_number t))
+        with e when Errors.noncritical e -> default false t)
    | Kvar s -> [],Oatom s
    | Kapp(Zopp,[t]) ->
        let tac,t' = transform (P_APP 1 :: p) t in
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index f0ca3bb9..216a719d 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -221,7 +221,10 @@ let compute_rhs bodyi index_of_f =
 (*s Now the function [compute_ivs] itself *)
 
 let compute_ivs gl f cs =
-  let cst = try destConst f with _ -> i_can't_do_that () in
+  let cst =
+    try destConst f
+    with e when Errors.noncritical e -> i_can't_do_that ()
+  in
   let body = Environ.constant_value (Global.env()) cst in
   match decomp_term body with
     | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) ->
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index ae73069d..7b0d96bb 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -292,7 +292,8 @@ let unbox = function
 (* Protects the convertibility test against undue exceptions when using it
    with untyped terms *)
 
-let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false
+let safe_pf_conv_x gl c1 c2 =
+  try pf_conv_x gl c1 c2 with e when Errors.noncritical e -> false
 
 
 (* Add a Ring or a Semi-Ring to the database after a type verification *)
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index e810e15c..fb45e816 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -335,7 +335,7 @@ let parse_term t =
     | Kapp("Z.succ",[t]) -> Tsucc t
     | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
-	(try Tnum (recognize t) with _ -> Tother)
+	(try Tnum (recognize t) with e when Errors.noncritical e -> Tother)
     | _ -> Tother
   with e when Logic.catchable_exception e -> Tother
 
@@ -357,6 +357,6 @@ let is_scalar t =
     | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
     | _ -> false in
-  try aux t with _ -> false
+  try aux t with e when Errors.noncritical e -> false
 
 end
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 4a6d462e..e57230cb 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -225,7 +225,8 @@ let add_reified_atom t env =
     env.terms <- env.terms @ [t]; i
 
 let get_reified_atom env =
-  try List.nth env.terms with _ -> failwith "get_reified_atom"
+  try List.nth env.terms
+  with e when Errors.noncritical e -> failwith "get_reified_atom"
 
 (* \subsection{Gestion de l'environnement de proposition pour Omega} *)
 (* ajout d'une proposition *)
@@ -235,7 +236,9 @@ let add_prop env t =
     let i = List.length env.props in  env.props <- env.props @ [t]; i
 
 (* accès a une proposition *)
-let get_prop v env = try List.nth v env with _ -> failwith "get_prop"
+let get_prop v env =
+  try List.nth v env
+  with e when Errors.noncritical e -> failwith "get_prop"
 
 (* \subsection{Gestion du nommage des équations} *)
 (* Ajout d'une equation dans l'environnement de reification *)
@@ -247,7 +250,8 @@ let add_equation env e =
 (* accès a une equation *)
 let get_equation env id =
   try Hashtbl.find env.equations id
-  with e -> Printf.printf "Omega Equation %d non trouvée\n" id; raise e
+  with Not_found as e ->
+    Printf.printf "Omega Equation %d non trouvée\n" id; raise e
 
 (* Affichage des termes réifiés *)
 let rec oprint ch = function
@@ -349,7 +353,8 @@ let rec reified_of_formula env = function
       app coq_t_minus [| reified_of_formula env t1; reified_of_formula env t2 |]
 
 let reified_of_formula env f =
-  begin try reified_of_formula env f with e -> oprint stderr f; raise e end
+  try reified_of_formula env f
+  with reraise -> oprint stderr f; raise reraise
 
 let rec reified_of_proposition env = function
     Pequa (_,{ e_comp=Eq; e_left=t1; e_right=t2 }) ->
@@ -380,8 +385,8 @@ let rec reified_of_proposition env = function
   | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |]
 
 let reified_of_proposition env f =
-  begin try reified_of_proposition env f
-  with e -> pprint stderr f; raise e end
+  try reified_of_proposition env f
+  with reraise -> pprint stderr f; raise reraise
 
 (* \subsection{Omega vers COQ réifié} *)
 
@@ -397,11 +402,11 @@ let reified_of_omega env body constant =
   List.fold_right mk_coeff body coeff_constant
 
 let reified_of_omega env body c  =
-  begin try
+  try
     reified_of_omega env body c
-  with e ->
-    display_eq display_omega_var (body,c); raise e
-  end
+  with reraise ->
+    display_eq display_omega_var (body,c); raise reraise
+
 
 (* \section{Opérations sur les équations}
 Ces fonctions préparent les traces utilisées par la tactique réfléchie
@@ -1000,10 +1005,11 @@ let rec solve_with_constraints all_solutions path =
   let weighted = filter_compatible_systems path all_solutions in
   let (winner_sol,winner_deps) =
     try select_smaller weighted
-    with e ->
+    with reraise ->
       Printf.printf "%d - %d\n"
 	(List.length weighted) (List.length all_solutions);
-      List.iter display_depend path; raise e in
+      List.iter display_depend path; raise reraise
+  in
   build_tree winner_sol (List.rev path) winner_deps
 
 let find_path {o_hyp=id;o_path=p} env =
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 956ccf09..6e7a8d32 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -90,7 +90,8 @@ VERNAC COMMAND EXTEND Subtac
 
 let try_catch_exn f e =
   try f e
-  with exn -> errorlabstrm "Program" (Errors.print exn)
+  with exn when Errors.noncritical exn ->
+    errorlabstrm "Program" (Errors.print exn)
 
 let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e
 let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 281e981b..ad248bfb 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -221,6 +221,6 @@ let subtac (loc, command) =
   | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
      Loc.Exc_located (loc, e') as e) -> raise e
 
-  | e -> 
+  | reraise ->
       (*       msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
-      raise e
+      raise reraise
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 221b57ee..0b1ed9bb 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -342,7 +342,7 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
       let pred = predicate 0 c in
       let env' = push_rel_context (context_of_arsign arsign) env in
 	ignore(Typing.sort_of env' evm pred); pred
-    with _ -> lift nar c
+    with e when Errors.noncritical e -> lift nar c
 
 module Cases_F(Coercion : Coercion.S) : S = struct
 
@@ -1465,7 +1465,8 @@ let extract_arity_signatures env0 tomatchl tmsign =
 	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
 	  let arsign = fst (get_arity env0 indf) in
 	    (na,None,build_dependent_inductive env0 indf)
-	    ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign with _ -> assert false) in
+	    ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign
+              with e when Errors.noncritical e -> assert false) in
   let rec buildrec = function
     | [],[] -> []
     | (_,tm)::ltm, x::tmsign ->
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 168a799d..0c03fb4c 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -356,7 +356,7 @@ module Coercion = struct
 		     jres),
 		jres.uj_type)
              (hj,typ_cl) p)
-    with _ -> anomaly "apply_coercion"
+    with e when Errors.noncritical e -> anomaly "apply_coercion"
 
   let inh_app_fun env isevars j =
     let isevars = ref isevars in
@@ -506,5 +506,5 @@ module Coercion = struct
 	    with NoSubtacCoercion ->
 	      error_cannot_coerce env' isevars (t, t'))
 	else isevars
-      with _ -> isevars
+      with e when Errors.noncritical e -> isevars
 end
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 14a09032..537a8301 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -248,7 +248,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
 	  | [(_, None, t); (_, None, u)], Sort (Prop Null)
 	      when Reductionops.is_conv env !isevars t u -> t
 	  | _, _ -> error ()
-      with _ -> error ()
+      with e when Errors.noncritical e -> error ()
   in
   let measure = interp_casted_constr isevars binders_env measure relargty in
   let wf_rel, wf_rel_fun, measure_fn =
@@ -440,7 +440,7 @@ let interp_recursive fixkind l =
       let sort = Retyping.get_type_of env !evdref t in
       let fixprot =
 	try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|])
-	with e -> t
+	with e when Errors.noncritical e -> t
       in
 	(id,None,fixprot) :: env')
       [] fixnames fixtypes
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index dfcc8526..d8f46098 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -121,7 +121,7 @@ let obl_substitution expand obls deps =
        let xobl = obls.(x) in
        let oblb =
 	 try get_obligation_body expand xobl
-	 with _ -> assert(false)
+	 with e when Errors.noncritical e -> assert(false)
        in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
     deps []
 
@@ -498,7 +498,8 @@ let rec solve_obligation prg num tac =
 		let obls = Array.copy obls in
 		let _ = obls.(num) <- obl in
 		let res = try update_obls prg obls (pred rem)
-		  with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e))
+		  with e when Errors.noncritical e ->
+                    pperror (Errors.print (Cerrors.process_vernac_interp_error e))
 		in
 		  match res with
 		  | Remain n when n > 0 ->
@@ -552,7 +553,7 @@ and solve_obligation_by_tac prg obls i tac =
 	| Refiner.FailError (_, s) ->
 	    user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
 	| Util.Anomaly _ as e -> raise e
-	| e -> false
+	| e when Errors.noncritical e -> false
 
 and solve_prg_obligations prg ?oblset tac =
   let obls, rem = prg.prg_obligations in
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 95e756ab..f0579711 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -302,7 +302,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | GCoFix i ->
 	      let cofix = (i,(names,ftys,fdefs)) in
-	      (try check_cofix env cofix with e -> Loc.raise loc e);
+	      (try check_cofix env cofix
+               with e when Errors.noncritical e -> Loc.raise loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
@@ -601,7 +602,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	     ~split:true ~fail:true env !evdref;
 	   evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
 	     ~split:true ~fail:false env !evdref
-	 with e -> if fail_evar then raise e else ());
+	 with e when Errors.noncritical e ->
+           if fail_evar then raise e else ());
       evdref := consider_remaining_unif_problems env !evdref;
       let c = if expand_evar then nf_evar !evdref c' else c' in
       if fail_evar then check_evars env Evd.empty !evdref c;
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index fbb44811..e32bb9e0 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -232,7 +232,7 @@ let build_dependent_sum l =
 	let hyptype = substl names t in
 	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
 	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
-	   with _ -> ());
+	   with e when Errors.noncritical e -> ());
 	let tac = assert_tac (Name n) hyptype in
 	let conttac =
 	  (fun cont ->
@@ -331,7 +331,7 @@ let destruct_ex ext ex =
 	       Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 ->
 		 let (dom, rng) =
 		   try (args.(0), args.(1))
-		   with _ -> assert(false)
+		   with e when Errors.noncritical e -> assert(false)
 		 in
 		 let pi1 = (mk_ex_pi1 dom rng acc) in
 		 let rng_body =
@@ -375,9 +375,9 @@ let solve_by_tac evi t =
       Inductiveops.control_only_guard (Global.env ())
 	const.Entries.const_entry_body;
       const.Entries.const_entry_body
-  with e ->
+  with reraise ->
     Pfedit.delete_current_proof();
-    raise e
+    raise reraise
 
 (* let apply_tac t goal = t goal *)
 
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index da0a65ff..a14eda60 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -349,7 +349,7 @@ let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids
          if computeinnertypes then
 try
           Acic.CicHash.find terms_to_types tt
-with _ ->
+with e when e <> Sys.Break ->
 (*CSC: Warning: it really happens, for example in Ring_theory!!! *)
 Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-type-inference: ") (Printer.pr_lconstr tt)) ; assert false
          else
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index a21a919a..c22c16f0 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -147,7 +147,8 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
 (*CSC: universes.                                                        *)
 (try
         Typeops.judge_of_type u
- with _ -> (* Successor of a non universe-variable universe anomaly *)
+ with e when e <> Sys.Break ->
+ (* Successor of a non universe-variable universe anomaly *)
  (Pp.ppnl (Pp.str "Warning: universe refresh performed!!!") ; flush stdout ) ;
   Typeops.judge_of_type (Termops.new_univ ())
 )
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 1037bbf0..867aac71 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -143,7 +143,7 @@ let rec join_dirs cwd =
   | he::tail ->
       (try
         Unix.mkdir cwd 0o775
-       with _ -> () (* Let's ignore the errors on mkdir *)
+       with e when e <> Sys.Break -> () (* Let's ignore the errors on mkdir *)
       ) ;
      let newcwd = cwd ^ "/" ^ he in
       join_dirs newcwd tail
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bdf94e0d..86f96c7c 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -126,7 +126,7 @@ module Default = struct
 		     jres),
 		jres.uj_type)
              (hj,typ_cl) p)
-    with _ -> anomaly "apply_coercion"
+    with e when Errors.noncritical e -> anomaly "apply_coercion"
 
   let inh_app_fun env evd j =
     let t = whd_betadeltaiota env evd j.uj_type in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a74e4cb4..0166b64c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -272,7 +272,7 @@ let is_nondep_branch c n =
   try
     let sign,ccl = decompose_lam_n_assum n c in
     noccur_between 1 (rel_context_length sign) ccl
-  with _ -> (* Not eta-expanded or not reduced *)
+  with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
     false
 
 let extract_nondep_branches test c b n =
@@ -386,7 +386,7 @@ let rec detype (isgoal:bool) avoid env t =
     | Var id ->
 	(try
 	  let _ = Global.lookup_named id in GRef (dl, VarRef id)
-	 with _ ->
+	 with e when Errors.noncritical e ->
 	  GVar (dl, id))
     | Sort s -> GSort (dl,detype_sort s)
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
@@ -492,7 +492,7 @@ and detype_eqns isgoal avoid env ci computable constructs consnargsl bl =
     let mat = build_tree Anonymous isgoal (avoid,env) ci bl in
     List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c))
       mat
-  with _ ->
+  with e when Errors.noncritical e ->
     Array.to_list
       (array_map3 (detype_eqn isgoal avoid env) constructs consnargsl bl)
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 14f35941..0eed1949 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -454,7 +454,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 		 else Evd.set_leq_sort evd s1 s2 
 	       in (evd', true)
 	     with Univ.UniverseInconsistency _ -> (evd, false)
-	     | _ -> (evd, false))
+	     | e when Errors.noncritical e -> (evd, false))
 
 	| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
             ise_and evd
@@ -730,12 +730,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
   let (term2,l2 as appr2) = decompose_app t2 in
   match kind_of_term term1, kind_of_term term2 with
   | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = []
-      & array_for_all (fun a -> eq_constr a term2 or isEvar a) args1 ->
+      & List.for_all (fun a -> eq_constr a term2 or isEvar a)
+        (remove_instance_local_defs evd evk1 (Array.to_list args1)) ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
     choose_less_dependent_instance evk1 evd term2 args1
   | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = []
-      & array_for_all (fun a -> eq_constr a term1 or isEvar a) args2 ->
+      & List.for_all (fun a -> eq_constr a term1 or isEvar a)
+        (remove_instance_local_defs evd evk2 (Array.to_list args2)) ->
       (* The typical kind of constraint coming from pattern-matching return
          type inference *)
     choose_less_dependent_instance evk2 evd term1 args2
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b0248a84..fc29ba6c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1194,10 +1194,9 @@ let filter_candidates evd evk filter candidates =
 
 let closure_of_filter evd evk filter =
   let evi = Evd.find_undefined evd evk in
-  let vars = collect_vars (evar_concl evi) in
-  let ids = List.map pi1 (evar_context evi) in
-  let test id b = b || Idset.mem id vars in
-  let newfilter = List.map2 test ids filter in
+  let vars = collect_vars (nf_evar evd (evar_concl evi)) in
+  let test (id,c,_) b = b || Idset.mem id vars || c <> None in
+  let newfilter = List.map2 test (evar_context evi) filter in
   if newfilter = evar_filter evi then None else Some newfilter
 
 let restrict_hyps evd evk filter candidates =
@@ -1352,9 +1351,14 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
   let f,args = decompose_app_vect t in
   match kind_of_term f with
   | Construct (ind,_) ->
-      let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
-      let params,_ = array_chop nparams args in
-      array_for_all (is_constrainable_in k g) params
+      let nparams =
+        (fst (Global.lookup_inductive ind)).Declarations.mind_nparams
+      in
+      if nparams > Array.length args
+      then true (* We don't try to be more clever *)
+      else
+        let params,_ = array_chop nparams args in
+        array_for_all (is_constrainable_in k g) params
   | Ind _ -> array_for_all (is_constrainable_in k g) args
   | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
   | Evar (ev',_) -> ev' <> ev (*If ev' needed, one may also try to restrict it*)
@@ -1442,7 +1446,7 @@ let check_evar_instance evd evk1 body conv_algo =
   (* FIXME: The body might be ill-typed when this is called from w_merge *)
   let ty =
     try Retyping.get_type_of evenv evd body
-    with _ -> error "Ill-typed evar instance"
+    with e when Errors.noncritical e -> error "Ill-typed evar instance"
   in
   let evd,b = conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl in
   if b then evd else
@@ -1492,7 +1496,10 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
           (filter_compatible_candidates conv_algo env evd evi args rhs) l in
       match l' with
       | [] -> error_cannot_unify env evd (mkEvar ev, rhs)
-      | [c,evd] -> Evd.define evk c evd
+      | [c,evd] ->
+          (* solve_candidates might have been called recursively in the mean *)
+          (* time and the evar been solved by the filtering process *)
+          if Evd.is_undefined evd evk then Evd.define evk c evd else evd
       | l when List.length l < List.length l' ->
           let candidates = List.map fst l in
           restrict_evar evd evk None (Some candidates)
@@ -1643,7 +1650,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
                   map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
 	            imitate envk t in
                 t::l
-              with _ -> l in
+              with e when Errors.noncritical e -> l in
             (match candidates with
             | [x] -> x
             | _ ->
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 2b326fd1..591a008c 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -230,3 +230,4 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun ->
   evar_map
 
+val remove_instance_local_defs : evar_map -> existential_key -> constr list -> constr list
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 6d5c98ce..4d9eb897 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -67,9 +67,12 @@ let evar_hyps evi = evi.evar_hyps
 let evar_context evi = named_context_of_val evi.evar_hyps
 let evar_body evi = evi.evar_body
 let evar_filter evi = evi.evar_filter
-let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps
 let evar_filtered_context evi =
   snd (list_filter2 (fun b c -> b) (evar_filter evi,evar_context evi))
+let evar_filtered_hyps evi =
+  List.fold_right push_named_context_val (evar_filtered_context evi)
+    empty_named_context_val
+let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps
 let evar_env evi =
   List.fold_right push_named (evar_filtered_context evi)
     (reset_context (Global.env()))
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 4813d3b9..dbaf803b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -127,6 +127,7 @@ val evar_concl : evar_info -> constr
 val evar_context : evar_info -> named_context
 val evar_filtered_context : evar_info -> named_context
 val evar_hyps : evar_info -> named_context_val
+val evar_filtered_hyps : evar_info -> named_context_val
 val evar_body : evar_info -> evar_body
 val evar_filter : evar_info -> bool list
 val evar_unfiltered_env :  evar_info -> env
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index bb0a0e92..bdccc57b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -290,6 +290,7 @@ let find_rectype env sigma c =
   match kind_of_term t with
     | Ind ind ->
         let (mib,mip) = Inductive.lookup_mind_specif env ind in
+        if mib.mind_nparams > List.length l then raise Not_found;
         let (par,rargs) = list_chop mib.mind_nparams l in
         IndType((ind, par),rargs)
     | _ -> raise Not_found
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d8678371..1dd71fab 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -69,8 +69,9 @@ let search_guard loc env possible_indexes fixdefs =
   if List.for_all (fun l->1=List.length l) possible_indexes then
     let indexes = Array.of_list (List.map List.hd possible_indexes) in
     let fix = ((indexes, 0),fixdefs) in
-    (try check_fix env fix with
-       | e -> if loc = dummy_loc then raise e else Loc.raise loc e);
+    (try check_fix env fix
+     with e when Errors.noncritical e ->
+       if loc = dummy_loc then raise e else Loc.raise loc e);
     indexes
   else
     (* we now search recursively amoungst all combinations *)
@@ -109,7 +110,8 @@ let resolve_evars env evdref fail_evar resolve_classes =
   (* Resolve eagerly, potentially making wrong choices *)
   evdref := (try consider_remaining_unif_problems
 	       ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
-	     with e -> if fail_evar then raise e else !evdref)
+	     with e when Errors.noncritical e ->
+               if fail_evar then raise e else !evdref)
 
 let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
   let evdref = ref evd in
@@ -441,7 +443,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | GCoFix i ->
 	      let cofix = (i,(names,ftys,fdefs)) in
-	      (try check_cofix env cofix with e -> Loc.raise loc e);
+	      (try check_cofix env cofix
+               with e when Errors.noncritical e -> Loc.raise loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 0f04549f..434fe80c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -207,16 +207,16 @@ let cs_pattern_of_constr t =
   match kind_of_term t with
       App (f,vargs) ->
 	begin
-	  try  Const_cs (global_of_constr f) , -1, Array.to_list vargs with
-	      _ -> raise Not_found
+	  try  Const_cs (global_of_constr f) , -1, Array.to_list vargs
+          with e when Errors.noncritical e -> raise Not_found
 	end
     | Rel n -> Default_cs, pred n, []
     | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b]
     | Sort s -> Sort_cs (family_of_sort s), -1, []
     | _ ->
 	begin
-	  try  Const_cs (global_of_constr t) , -1, [] with
-	      _ -> raise Not_found
+	  try  Const_cs (global_of_constr t) , -1, []
+          with e when Errors.noncritical e -> raise Not_found
 	end
 
 (* Intended to always succeed *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index fddc7fc7..993ad46b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -924,7 +924,10 @@ let meta_reducible_instance evd b =
     let u = whd_betaiota Evd.empty u in
     match kind_of_term u with
     | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
-	let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
+	let m =
+          try destMeta c
+          with e when Errors.noncritical e -> destMeta (pi1 (destCast c))
+        in
 	(match
 	  try
 	    let g,s = List.assoc m metas in
@@ -934,7 +937,10 @@ let meta_reducible_instance evd b =
 	    | Some g -> irec (mkCase (ci,p,g,bl))
 	    | None -> mkCase (ci,irec p,c,Array.map irec bl))
     | App (f,l) when isMeta f or isCast f & isMeta (pi1 (destCast f)) ->
-	let m = try destMeta f with _ -> destMeta (pi1 (destCast f)) in
+        let m =
+          try destMeta f
+          with e when Errors.noncritical e -> destMeta (pi1 (destCast f))
+        in
 	(match
 	  try
 	    let g,s = List.assoc m metas in
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index f16eed6c..3b679fce 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -30,12 +30,12 @@ let rec subst_type env sigma typ = function
 (* et sinon on substitue *)
 
 let sort_of_atomic_type env sigma ft args =
-  let rec concl_of_arity env ar =
-    match kind_of_term (whd_betadeltaiota env sigma ar) with
-    | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
-    | Sort s -> s
-    | _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args))
-  in concl_of_arity env ft
+  let rec concl_of_arity env ar args =
+    match kind_of_term (whd_betadeltaiota env sigma ar), args with
+    | Prod (na, t, b), h::l -> concl_of_arity (push_rel (na,Some h,t) env) b l
+    | Sort s, [] -> s
+    | _ -> anomaly "Not a sort"
+  in concl_of_arity env ft (Array.to_list args)
 
 let type_of_var env id =
   try let (_,_,ty) = lookup_named id env in ty
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index b43b9adb..78b239c0 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -125,12 +125,12 @@ type constant_evaluation =
 
 (* We use a cache registered as a global table *)
 
-let eval_table = ref Cmap.empty
+let eval_table = ref Cmap_env.empty
 
-type frozen = (int * constant_evaluation) Cmap.t
+type frozen = (int * constant_evaluation) Cmap_env.t
 
 let init () =
-  eval_table := Cmap.empty
+  eval_table := Cmap_env.empty
 
 let freeze () =
   !eval_table
@@ -291,10 +291,10 @@ let compute_consteval sigma env ref =
 let reference_eval sigma env = function
   | EvalConst cst as ref ->
       (try
-	 Cmap.find cst !eval_table
+	 Cmap_env.find cst !eval_table
        with Not_found -> begin
 	 let v = compute_consteval sigma env ref in
-	 eval_table := Cmap.add cst v !eval_table;
+	 eval_table := Cmap_env.add cst v !eval_table;
 	 v
        end)
   | ref -> compute_consteval sigma env ref
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b78850d3..0344ebcc 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -118,7 +118,7 @@ let _ =
 
 let class_info c =
   try Gmap.find c !classes
-  with _ -> not_a_class (Global.env()) (constr_of_global c)
+  with Not_found -> not_a_class (Global.env()) (constr_of_global c)
 
 let global_class_of_constr env c =
   try class_info (global_of_constr c)
@@ -132,7 +132,9 @@ let dest_class_arity env c =
   let rels, c = Term.decompose_prod_assum c in
     rels, dest_class_app env c
 
-let class_of_constr c = try Some (dest_class_arity (Global.env ()) c) with _ -> None
+let class_of_constr c =
+  try Some (dest_class_arity (Global.env ()) c)
+  with e when Errors.noncritical e -> None
 
 let rec is_class_type evd c =
   match kind_of_term c with
@@ -215,7 +217,7 @@ let rebuild_class cl =
   try 
     let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
       set_typeclass_transparency cst false false; cl
-  with _ -> cl
+  with e when Errors.noncritical e -> cl
 
 let class_input : typeclass -> obj =
   declare_object
@@ -238,7 +240,7 @@ let check_instance env sigma c =
     let (evd, c) = resolve_one_typeclass env sigma
       (Retyping.get_type_of env sigma c) in
       Evd.is_empty (Evd.undefined_evars evd)
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 let build_subclasses ~check env sigma glob pri =
   let rec aux pri c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 63cdb378..df5eff6a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -430,8 +430,9 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 		 then Evd.set_leq_sort sigma s1 s2 
 		 else Evd.set_eq_sort sigma s1 s2 
 	       in (sigma', metasubst, evarsubst)
-	     with _ -> error_cannot_unify curenv sigma (m,n))
-	      
+	     with e when Errors.noncritical e ->
+               error_cannot_unify curenv sigma (m,n))
+
 	| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
 	    unirec_rec (push (na,t1) curenvnb) CONV true wt
 	      (unirec_rec curenvnb CONV true false substn t1 t2) c1 c2
@@ -708,10 +709,12 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
       else (right, st2, res)
   | (IsSuperType,IsSubType) ->
     (try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1)
-     with _ -> (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
+     with e when Errors.noncritical e ->
+       (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
   | (IsSubType,IsSuperType) ->
     (try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2)
-     with _ -> (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
+     with e when Errors.noncritical e ->
+       (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
     
 (* Unification
  *
@@ -913,7 +916,7 @@ let w_merge env with_types flags (evd,metas,evars) =
 	let rec process_eqns failures = function
 	  | (mv,status,c)::eqns ->
               (match (try Inl (unify_type env evd flags mv status c)
-		      with e -> Inr e)
+		      with e when Errors.noncritical e -> Inr e)
 	       with 
 	       | Inr e -> process_eqns (((mv,status,c),e)::failures) eqns
 	       | Inl (evd,metas,evars) ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 00efa981..3966146d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -44,7 +44,7 @@ let invert_tag cst tag reloc_tbl =
 let find_rectype_a env c =
   let (t, l) =
     let t = whd_betadeltaiota env c in
-    try destApp t with _ -> (t,[||]) in
+    try destApp t with e when Errors.noncritical e -> (t,[||]) in
   match kind_of_term t with
   | Ind ind -> (ind, l)
   | _ -> raise Not_found
@@ -176,7 +176,10 @@ and nf_stk env c t stk  =
       nf_stk env (mkApp(c,args)) t stk
   | Zfix (f,vargs) :: stk ->
       let fa, typ = nf_fix_app env f vargs in
-      let _,_,codom = try decompose_prod env typ with _ -> exit 120 in
+      let _,_,codom =
+        try decompose_prod env typ
+        with e when Errors.noncritical e -> exit 120
+      in
       nf_stk env (mkApp(fa,[|c|])) (subst1 c codom) stk
   | Zswitch sw :: stk ->
       let (mind,_ as ind),allargs = find_rectype_a env t in
@@ -206,7 +209,10 @@ and nf_predicate env ind mip params v pT =
   | Vfun f, Prod _ ->
       let k = nb_rel env in
       let vb = body_of_vfun k f in
-      let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in
+      let name,dom,codom =
+        try decompose_prod env pT
+        with e when Errors.noncritical e -> exit 121
+      in
       let dep,body =
 	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
       dep, mkLambda(name,dom,body)
@@ -228,7 +234,10 @@ and nf_args env vargs t =
   let args =
     Array.init len
       (fun i ->
-	let _,dom,codom = try decompose_prod env !t with _ -> exit 123 in
+	let _,dom,codom =
+          try decompose_prod env !t
+          with e when Errors.noncritical e -> exit 123
+        in
 	let c = nf_val env (arg vargs i) dom in
 	t := subst1 c codom; c) in
   !t,args
@@ -239,7 +248,10 @@ and nf_bargs env b t =
   let args =
     Array.init len
       (fun i ->
-	let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
+	let _,dom,codom =
+          try decompose_prod env !t
+          with e when Errors.noncritical e -> exit 124
+        in
 	let c = nf_val env (bfield b i) dom in
 	t := subst1 c codom; c) in
   args
@@ -249,7 +261,7 @@ and nf_fun env f typ =
   let vb = body_of_vfun k f in
   let name,dom,codom =
     try decompose_prod env typ
-    with _ ->
+    with e when Errors.noncritical e ->
       raise (Type_errors.TypeError(env,Type_errors.ReferenceVariables typ))
   in
   let body = nf_val (push_rel (name,None,dom) env) vb codom in
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 4462062c..f271a6bd 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -42,7 +42,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
   let sigma',typed_c =
     try Pretyping.Default.understand_ltac ~resolve_classes:true true sigma env ltac_var
 	  (Pretyping.OfType (Some evi.evar_concl)) rawc
-    with _ ->
+    with e when Errors.noncritical e ->
       let loc = Glob_term.loc_of_glob_constr rawc in
       user_err_loc
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
diff --git a/proofs/goal.ml b/proofs/goal.ml
index dc1ac5dd..37ebce67 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -276,7 +276,7 @@ let check_typability env sigma c =
 
 let recheck_typability (what,id) env sigma t =
   try check_typability env sigma t
-  with _ ->
+  with e when Errors.noncritical e ->
     let s = match what with
       | None -> "the conclusion"
       | Some id -> "hypothesis "^(Names.string_of_id id) in
@@ -474,7 +474,7 @@ module V82 = struct
   (* Old style hyps primitive *)
   let hyps evars gl =
     let evi = content evars gl in
-    evi.Evd.evar_hyps
+    Evd.evar_filtered_hyps evi
 
   (* Access to ".evar_concl" *)
   let concl evars gl =
@@ -554,10 +554,16 @@ module V82 = struct
        with a good implementation of them.
     *)
       
-  (* Used for congruence closure *)
-  let new_goal_with sigma gl new_hyps =
+  (* Used for congruence closure and change *)
+  let new_goal_with sigma gl extra_hyps =
     let evi = content sigma gl in
-    let new_evi = { evi with Evd.evar_hyps = new_hyps } in
+    let hyps = evi.Evd.evar_hyps in
+    let new_hyps =
+      List.fold_right Environ.push_named_context_val extra_hyps hyps in
+    let extra_filter = List.map (fun _ -> true) extra_hyps in
+    let new_filter = extra_filter @ evi.Evd.evar_filter in
+    let new_evi =
+      { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
     let new_evi = Typeclasses.mark_unresolvable new_evi in
     let evk = Evarutil.new_untyped_evar () in
     let new_sigma = Evd.add Evd.empty evk new_evi in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 9cd439ab..c0a094d3 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -232,7 +232,7 @@ module V82 : sig
   val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
  (* Used for congruence closure *)
-  val new_goal_with : Evd.evar_map -> goal ->  Environ.named_context_val -> goal Evd.sigma 
+  val new_goal_with : Evd.evar_map -> goal -> Sign.named_context -> goal Evd.sigma
 
   (* Used by the compatibility layer and typeclasses *)
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
diff --git a/proofs/logic.ml b/proofs/logic.ml
index d240c1e1..497ab1fa 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -105,7 +105,7 @@ let clear_hyps sigma ids sign cl =
 
 let recheck_typability (what,id) env sigma t =
   try check_typability env sigma t
-  with _ ->
+  with e when Errors.noncritical e ->
     let s = match what with
       | None -> "the conclusion"
       | Some id -> "hypothesis "^(string_of_id id) in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 45e4a84e..7bac87d2 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -68,7 +68,7 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook =
    | None -> Proofview.tclUNIT ()
   in
   try Proof_global.run_tactic tac
-  with e -> Proof_global.discard_current (); raise e
+  with reraise -> Proof_global.discard_current (); raise reraise
 
 let restart_proof () = undo_todepth 1
 
@@ -164,9 +164,9 @@ let build_constant_by_tactic id sign typ tac =
     let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
     delete_current_proof ();
     const
-  with e ->
+  with reraise ->
     delete_current_proof ();
-    raise e
+    raise reraise
 
 let build_by_tactic env typ tac =
   let id = id_of_string ("temporary_proof"^string_of_int (next())) in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index a4e556c5..012a4dc1 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -323,7 +323,7 @@ let rec rollback pr =
 let transaction pr t =
   init_transaction pr;
   try t (); commit pr
-  with e -> rollback pr; raise e
+  with reraise -> rollback pr; raise reraise
 
 
 (* Focus command (focuses on the [i]th subgoal) *)
@@ -429,9 +429,9 @@ let run_tactic env tac pr =
     let tacticced_proofview = Proofview.apply env tac sp in
     pr.state <- { pr.state with proofview = tacticced_proofview };
     push_undo starting_point pr
-  with e -> 
+  with reraise ->
     restore_state starting_point pr;
-    raise e
+    raise reraise
 
 (*** Commands ***)
 
@@ -476,7 +476,7 @@ module V82 = struct
 	let new_proofview = Proofview.V82.instantiate_evar n com sp in
 	pr.state <- { pr.state with proofview = new_proofview };
 	push_undo starting_point pr
-      with e -> 
+      with reraise ->
 	restore_state starting_point pr;
-	raise e
+	raise reraise
 end
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 74e40e3b..d299a520 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -320,10 +320,12 @@ let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step ->
 (* takes a tactic which can raise exception and makes it pure by *failing* 
     on with these exceptions. Does not catch anomalies. *)
 let purify t = 
-  let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step
-     	                                                     with Util.Anomaly _ as e -> raise e
-							           | e -> sk (Util.Inr e) fk step
-	       }
+  let t' env =
+    { go = fun sk fk step ->
+      try (t env).go (fun x -> sk (Util.Inl x)) fk step
+      with Util.Anomaly _ as e -> raise e
+	| e when Errors.noncritical e -> sk (Util.Inr e) fk step
+    }
   in
   tclBIND t' begin function
     | Util.Inl x -> tclUNIT x
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 37c63644..21b43212 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -255,7 +255,7 @@ let tclORELSE0 t1 t2 g =
   try
     t1 g
   with (* Breakpoint *)
-    | e -> catch_failerror e; t2 g
+    | e when Errors.noncritical e -> catch_failerror e; t2 g
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
    then applies t2 *)
@@ -267,7 +267,7 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
 let tclORELSE_THEN t1 t2then t2else gls =
   match
     try Some(tclPROGRESS t1 gls)
-    with e -> catch_failerror e; None
+    with e when Errors.noncritical e -> catch_failerror e; None
   with
     | None -> t2else gls
     | Some sgl ->
@@ -298,7 +298,7 @@ let ite_gen tcal tac_if continue tac_else gl=
     try
       tcal tac_if0 continue gl
     with (* Breakpoint *)
-      | e -> catch_failerror e; tac_else0 e gl
+      | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl
 
 (* Try the first tactic and, if it succeeds, continue with
    the second one, and if it fails, use the third one *)
@@ -352,7 +352,7 @@ let tclTIMEOUT n t g =
     | TacTimeout | Loc.Exc_located(_,TacTimeout) ->
       restore_timeout ();
       errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!")
-    | e -> restore_timeout (); raise e
+    | reraise -> restore_timeout (); raise reraise
 
 (* Beware: call by need of CAML, g is needed *)
 let rec tclREPEAT t g =
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index b56cb844..27ab990c 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -140,11 +140,11 @@ let debug_prompt lev g tac f =
     else (decr skip; run false; if !skip=0 then skipped:=0; DebugOn (lev+1)) in
   (* What to execute *)
   try f newlevel
-  with e ->
+  with reraise ->
     skip:=0; skipped:=0;
-    if Logic.catchable_exception e then
-      ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error e);
-    raise e
+    if Logic.catchable_exception reraise then
+      ppnl (str "Level " ++ int lev ++ str ": " ++ !explain_logic_error reraise);
+    raise reraise
 
 (* Prints a constr *)
 let db_constr debug env c =
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 5bc77457..b75984e3 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -45,8 +45,7 @@ let camlp4topobjs =
     [ "Camlp4Top.cmo";
       "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
       "Camlp4Parsers/Camlp4OCamlParser.cmo";
-      "Camlp4Parsers/Camlp4GrammarParser.cmo";
-      "q_util.cmo"; "q_coqast.cmo" ]
+      "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
 let topobjs = camlp4topobjs
 
 let gramobjs = []
@@ -257,8 +256,8 @@ let create_tmp_main_file modules =
     output_string oc "Coqtop.start();;\n";
     close_out oc;
     main_name
-  with e ->
-    clean main_name; raise e
+  with reraise ->
+    clean main_name; raise reraise
 
 (* main part *)
 let main () =
@@ -311,10 +310,10 @@ let main () =
 	clean main_file;
 	(* command gives the exit code in HSB, and signal in LSB !!! *)
 	if retcode > 255 then retcode lsr 8 else retcode
-  with e ->
-    clean main_file; raise e
+  with reraise ->
+    clean main_file; raise reraise
 
 let retcode =
-  try Printexc.print main () with _ -> 1
+  try Printexc.print main () with any -> 1
 
 let _ = exit retcode
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f7d63dcd..44fea151 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -829,7 +829,8 @@ let prepare_hint env (sigma,c) =
 
 let path_of_constr_expr c =
   match c with
-  | Topconstr.CRef r -> (try PathHints [global r] with _ -> PathAny)
+  | Topconstr.CRef r ->
+    (try PathHints [global r] with e when Errors.noncritical e -> PathAny)
   | _ -> PathAny
       
 let interp_hints h =
@@ -1170,9 +1171,9 @@ let tclLOG (dbg,depth,trace) pp tac =
 	  let out = tac gl in
 	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
 	  out
-	with e ->
+	with reraise ->
 	  msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
-	  raise e
+	  raise reraise
       end
     | Info ->
       (* For "info (trivial/auto)", we store a log trace *)
@@ -1181,9 +1182,9 @@ let tclLOG (dbg,depth,trace) pp tac =
 	  let out = tac gl in
 	  trace := (depth, Some pp) :: !trace;
 	  out
-	with e ->
+	with reraise ->
 	  trace := (depth, None) :: !trace;
-	  raise e
+	  raise reraise
       end
 
 (** For info, from the linear trace information, we reconstitute the part
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 039f022d..8e1d7cbf 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -208,8 +208,14 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl =
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
-  let base = try find_base rbase with _ -> HintDN.empty in
-  let max = try fst (Util.list_last (HintDN.find_all base)) with _ -> 0 in
+  let base =
+    try find_base rbase
+    with e when Errors.noncritical e -> HintDN.empty
+  in
+  let max =
+    try fst (Util.list_last (HintDN.find_all base))
+    with e when Errors.noncritical e -> 0
+  in
   let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
     rewtab:=Stringmap.add rbase (HintDN.union lrl base) !rewtab
 
@@ -248,7 +254,7 @@ let evd_convertible env evd x y =
   try
     ignore(Unification.w_unify ~flags:Unification.elim_flags env evd Reduction.CONV x y); true 
   (* try ignore(Evarconv.the_conv_x env x y evd); true *)
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 let decompose_applied_relation metas env sigma c ctype left2right =
   let find_rel ty =
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index cf4a267f..d05ae680 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -685,7 +685,7 @@ let resolve_typeclass_evars debug m env evd filter split fail =
   let evd = 
     try Evarconv.consider_remaining_unif_problems
       ~ts:(Typeclasses.classes_transparent_state ()) env evd
-    with _ -> evd
+    with e when Errors.noncritical e -> evd
   in
     resolve_all_evars debug m env (initial_select_evars filter) evd split fail
 
@@ -776,7 +776,10 @@ END
 
 let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
   try 
-    let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
+    let dbs = list_map_filter
+      (fun db -> try Some (Auto.searchtable_map db)
+        with e when Errors.noncritical e -> None) dbs
+    in
     let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
       eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
    with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 68dd5dba..6981a733 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -205,7 +205,8 @@ module SearchProblem = struct
 (* 	    let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
 (* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
 	      (lgls,pptac) :: aux tacl
-	  with e -> Refiner.catch_failerror e; aux tacl
+	  with e when Errors.noncritical e ->
+            Refiner.catch_failerror e; aux tacl
     in aux l
 
   (* Ordering of states is lexicographic on depth (greatest first) then
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a352355b..1c5e4b2f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -334,7 +334,8 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
 	  try
 	    rewrite_side_tac (!general_rewrite_clause cls
 				 lft2rgt occs (c,l) ~new_goals:[]) tac gl
-	  with e -> (* Try to see if there's an equality hidden *)
+	  with e when Errors.noncritical e ->
+            (* Try to see if there's an equality hidden *)
 	    let env' = push_rel_context rels env in
 	    let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
 	      match match_with_equality_type t' with
@@ -1156,7 +1157,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
                 ]
 (* not a dep eq or no decidable type found *)
             ) else (raise Not_dep_pair)
-        ) with _ ->
+        ) with e when Errors.noncritical e ->
 	  inject_at_positions env sigma u eq_clause posns
 	    (fun _ -> intros_pattern no_move ipats)
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f5fcb736..f6ecb47c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -606,7 +606,7 @@ let hResolve_auto id c t gl =
       hResolve id c n t gl
     with
     | UserError _ as e -> raise e
-    | _ -> resolve_auto (n+1)
+    | e when Errors.noncritical e -> resolve_auto (n+1)
   in
   resolve_auto 1
 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 47e3b7ca..c6f32ce2 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -64,9 +64,12 @@ let is_non_recursive_type t = op2bool (match_with_non_recursive_type t)
 
 (* Test dependencies *)
 
+(* NB: we consider also the let-in case in the following function,
+   since they may appear in types of inductive constructors (see #2629) *)
+
 let rec has_nodep_prod_after n c =
   match kind_of_term c with
-    | Prod (_,_,b) ->
+    | Prod (_,_,b) | LetIn (_,_,_,b) ->
 	( n>0 || not (dependent (mkRel 1) b))
 	&& (has_nodep_prod_after (n-1) b)
     | _            -> true
@@ -355,7 +358,10 @@ let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
 let coq_eq_true_pattern = lazy PATTERN [ %coq_eq_true_ref ?X1 ]
 
 let match_eq eqn eq_pat =
-  let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in
+  let pat =
+    try Lazy.force eq_pat
+    with e when Errors.noncritical e -> raise PatternMatchingFailure
+  in
   match matches pat eqn with
     | [(m1,t);(m2,x);(m3,y)] ->
 	assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b7f6addc..e4b3bdb1 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -497,7 +497,7 @@ let wrap_inv_error id = function
 (* The most general inversion tactic *)
 let inversion inv_kind status names id gls =
   try (raw_inversion inv_kind id status names) gls
-  with e -> wrap_inv_error id e
+  with e when Errors.noncritical e -> wrap_inv_error id e
 
 (* Specializing it... *)
 
@@ -540,7 +540,7 @@ let invIn k names ids id gls =
        inversion (false,k) NoDep names id;
        intros_replace_ids])
     gls
-  with e -> wrap_inv_error id e
+  with e when Errors.noncritical e -> wrap_inv_error id e
 
 let invIn_gen k names idl = try_intros_until (invIn k names idl)
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index b90a911a..98885af8 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -121,7 +121,7 @@ let is_applied_rewrite_relation env sigma rels t =
 	      let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in
 	      let _ = Typeclasses.resolve_one_typeclass env' evd inst in
 		Some (it_mkProd_or_LetIn t rels)
-	  with _ -> None)
+	  with e when Errors.noncritical e -> None)
   | _ -> None
 
 let _ =
@@ -145,11 +145,14 @@ let build_signature evars env m (cstrs : (types * types option) option list)
     new_cstr_evar evars env
       (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
   in
-  let mk_relty evars env ty obj =
+  let mk_relty evars newenv ty obj =
     match obj with
       | None | Some (_, None) ->
 	  let relty = mk_relation ty in
-	    new_evar evars env relty
+	    if closed0 ty then 
+	      let env' = Environ.reset_with_named_context (Environ.named_context_val env) env in
+		new_evar evars env' relty
+	    else new_evar evars newenv relty
       | Some (x, Some rel) -> evars, rel
   in
   let rec aux env evars ty l =
@@ -227,7 +230,7 @@ let cstrevars evars = snd evars
 
 let evd_convertible env evd x y =
   try ignore(Evarconv.the_conv_x env x y evd); true
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 let rec decompose_app_rel env evd t = 
   match kind_of_term t with
@@ -493,7 +496,7 @@ let rec apply_pointwise rel = function
   | [] -> rel
 
 let pointwise_or_dep_relation n t car rel =
-  if noccurn 1 car then
+  if noccurn 1 car && noccurn 1 rel then
     mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |])
   else
     mkApp (Lazy.force forall_relation, 
@@ -1048,7 +1051,8 @@ module Strategies =
 	let sigma, c = Constrintern.interp_open_constr (goalevars evars) env c in
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
-	  with _ -> error "fold: the term is not unfoldable !"
+	  with e when Errors.noncritical e ->
+            error "fold: the term is not unfoldable !"
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
@@ -1056,7 +1060,7 @@ module Strategies =
 	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
 			   rew_prf = RewCast DEFAULTcast; 
 			   rew_evars = sigma, cstrevars evars })
-	  with _ -> None
+	  with e when Errors.noncritical e -> None
 
     let fold_glob c : strategy =
       fun env avoid t ty cstr evars ->
@@ -1064,7 +1068,8 @@ module Strategies =
 	let sigma, c = Pretyping.Default.understand_tcc (goalevars evars) env c in
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
-	  with _ -> error "fold: the term is not unfoldable !"
+	  with e when Errors.noncritical e ->
+            error "fold: the term is not unfoldable !"
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
@@ -1072,7 +1077,7 @@ module Strategies =
 	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
 			   rew_prf = RewCast DEFAULTcast; 
 			   rew_evars = sigma, cstrevars evars })
-	  with _ -> None
+	  with e when Errors.noncritical e -> None
   
 
 end
@@ -1977,7 +1982,7 @@ let setoid_proof gl ty fn fallback =
       let evm = project gl in
       let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.type_of env evm rel)))) in
 	fn env evm car rel gl
-    with e ->
+    with e when Errors.noncritical e ->
       try fallback gl
       with Hipattern.NoEquationFound ->
 	  match e with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3ff0cf93..7479ee9a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -50,7 +50,7 @@ open Compat
 open Evd
 
 let safe_msgnl s =
-    try msgnl s with e ->
+    try msgnl s with e when Errors.noncritical e ->
       msgnl
 	(str "bug in the debugger: " ++
          str "an exception is raised while printing debug information")
@@ -92,7 +92,7 @@ let catch_error call_trace tac g =
   if call_trace = [] then tac g else try tac g with
   | LtacLocated _ as e -> raise e
   | Loc.Exc_located (_,LtacLocated _) as e -> raise e
-  | e ->
+  | e when Errors.noncritical e ->
     let (nrep,loc',c),tail = list_sep_last call_trace in
     let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
     if tail = [] then
@@ -569,13 +569,13 @@ let dump_glob_red_expr = function
     try
       Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
 	(Smartlocate.smart_global r)
-    with _ -> ()) occs
+    with e when Errors.noncritical e -> ()) occs
   | Cbv grf | Lazy grf ->
     List.iter (fun r ->
       try
         Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
 	  (Smartlocate.smart_global r)
-      with _ -> ()) grf.rConst
+      with e when Errors.noncritical e -> ()) grf.rConst
   | _ -> ()
 
 let intern_red_expr ist = function
@@ -1412,19 +1412,20 @@ let interp_may_eval f ist gl = function
   | ConstrTerm c ->
      try
 	f ist gl c
-     with e ->
-       debugging_exception_step ist false e (fun () ->
+     with reraise ->
+       debugging_exception_step ist false reraise (fun () ->
          str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c));
-       raise e
+       raise reraise
 
 (* Interprets a constr expression possibly to first evaluate *)
 let interp_constr_may_eval ist gl c =
   let (sigma,csr) =
     try
       interp_may_eval pf_interp_constr ist gl c
-    with e ->
-      debugging_exception_step ist false e (fun () -> str"evaluation of term");
-      raise e
+    with reraise ->
+      debugging_exception_step ist false reraise (fun () ->
+        str"evaluation of term");
+      raise reraise
   in
   begin
     db_constr ist.debug (pf_env gl) csr;
@@ -1762,10 +1763,7 @@ let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
 let pack_sigma (sigma,c) = {it=c;sigma=sigma}
 
 let extend_gl_hyps { it=gl ; sigma=sigma } sign =
-  let hyps = Goal.V82.hyps sigma gl in
-  let new_hyps = List.fold_right Environ.push_named_context_val sign hyps in
-  (* spiwack: (2010/01/13) if a bug was reintroduced in [change] in is probably here *)
-  Goal.V82.new_goal_with sigma gl new_hyps
+  Goal.V82.new_goal_with sigma gl sign
 
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist gl (tac:glob_tactic_expr) =
@@ -1925,9 +1923,11 @@ and interp_app loc ist gl fv largs =
 	    try
 	      catch_error trace
 		(val_interp {ist with lfun=newlfun@olfun; trace=trace} gl) body
-	    with e ->
-              debugging_exception_step ist false e (fun () -> str "evaluation");
-	      raise e in
+	    with reraise ->
+              debugging_exception_step ist false reraise
+                (fun () -> str "evaluation");
+	      raise reraise
+          in
 	  let gl = { gl with sigma=sigma } in
           debugging_step ist
 	    (fun () ->
@@ -2212,19 +2212,20 @@ and interp_match ist g lz constr lmr =
         (try
             let lmatch =
               try extended_matches c csr
-              with e ->
-                debugging_exception_step ist false e (fun () ->
+              with reraise ->
+                debugging_exception_step ist false reraise (fun () ->
                   str "matching with pattern" ++ fnl () ++
                   pr_constr_pattern_env (pf_env g) c);
-                raise e in
+                raise reraise
+            in
             try
               let lfun = extend_values_with_bindings lmatch ist.lfun in
               eval_with_fail { ist with lfun=lfun } lz g mt
-            with e ->
-              debugging_exception_step ist false e (fun () ->
+            with reraise ->
+              debugging_exception_step ist false reraise (fun () ->
                 str "rule body for pattern" ++
                 pr_constr_pattern_env (pf_env g) c);
-              raise e
+              raise reraise
          with e when is_match_catchable e ->
            debugging_step ist (fun () -> str "switching to the next rule");
            apply_match ist sigma csr tl)
@@ -2236,15 +2237,16 @@ and interp_match ist g lz constr lmr =
       errorlabstrm "Tacinterp.apply_match" (str
         "No matching clauses for match.") in
   let (sigma,csr) =
-      try interp_ltac_constr ist g constr with e ->
-        debugging_exception_step ist true e
+      try interp_ltac_constr ist g constr with reraise ->
+        debugging_exception_step ist true reraise
           (fun () -> str "evaluation of the matched expression");
-        raise e in
+        raise reraise in
   let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) sigma lmr in
   let res =
-     try apply_match ist sigma csr ilr with e ->
-       debugging_exception_step ist true e (fun () -> str "match expression");
-       raise e in
+     try apply_match ist sigma csr ilr with reraise ->
+       debugging_exception_step ist true reraise
+         (fun () -> str "match expression");
+       raise reraise in
   debugging_step ist (fun () ->
     str "match expression returns " ++ pr_value (Some (pf_env g)) (snd res));
   res
@@ -2404,6 +2406,7 @@ and interp_atomic ist gl tac =
 	(h_generalize_dep c_interp)
   | TacLetTac (na,c,clp,b,eqpat) ->
       let clp = interp_clause ist gl clp in
+      let eqpat = Option.map (interp_intro_pattern ist gl) eqpat in
       if clp = nowhere then
         (* We try to fully-typecheck the term *)
 	let (sigma,c_interp) = pf_interp_constr ist gl c in
@@ -3180,7 +3183,8 @@ let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t))
 let tacticIn t =
   globTacticIn (fun ist ->
     try glob_tactic (t ist)
-    with e -> anomalylabstrm "tacticIn"
+    with e when Errors.noncritical e ->
+      anomalylabstrm "tacticIn"
       (str "Incorrect tactic expression. Received exception is:" ++
        Errors.print e))
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 12292196..ac00a73d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1018,7 +1018,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
   let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
-    with err ->
+    with err when Errors.noncritical err ->
     try aux (clenv_push_prod clause)
     with NotExtensibleClause -> raise err in
   aux (make_clenv_binding gl (d,thm) lbind)
@@ -1708,7 +1708,7 @@ let make_pattern_test env sigma0 (sigma,c) =
   let flags = default_matching_flags sigma0 in
   let matching_fun t =
     try let sigma = w_unify env sigma Reduction.CONV ~flags c t in Some(sigma,t)
-    with _ -> raise NotUnifiable in
+    with e when Errors.noncritical e -> raise NotUnifiable in
   let merge_fun c1 c2 =
     match c1, c2 with
     | Some (_,c1), Some (_,c2) when not (is_fconv Reduction.CONV env sigma0 c1 c2) ->
@@ -2554,7 +2554,10 @@ let specialize_eqs id gl =
       
 
 let specialize_eqs id gl =
-  if try ignore(clear [id] gl); false with _ -> true then
+  if
+    (try ignore(clear [id] gl); false
+     with e when Errors.noncritical e -> true)
+  then
     tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl 
   else specialize_eqs id gl
 
@@ -2716,7 +2719,8 @@ let compute_elim_sig ?elimc elimt =
       | Some ( _,None,ind) ->
 	  let indhd,indargs = decompose_app ind in
 	  try {!res with indref = Some (global_of_constr indhd) }
-	  with _ -> error "Cannot find the inductive type of the inductive scheme.";;
+	  with e when Errors.noncritical e ->
+            error "Cannot find the inductive type of the inductive scheme.";;
 
 let compute_scheme_signature scheme names_info ind_type_guess =
   let f,l = decompose_app scheme.concl in
@@ -3551,4 +3555,5 @@ let unify ?(state=full_transparent_state) x y gl =
     in
     let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y
     in tclEVARS evd gl
-  with _ -> tclFAIL 0 (str"Not unifiable") gl
+  with e when Errors.noncritical e ->
+    tclFAIL 0 (str"Not unifiable") gl
diff --git a/test-suite/bugs/closed/2955.v b/test-suite/bugs/closed/2955.v
new file mode 100644
index 00000000..45e24b5f
--- /dev/null
+++ b/test-suite/bugs/closed/2955.v
@@ -0,0 +1,52 @@
+Require Import Coq.Arith.Arith.
+
+Module A.
+
+  Fixpoint foo (n:nat) :=
+  match n with
+  | 0 => 0
+  | S n => bar n
+  end
+
+  with bar (n:nat) :=
+  match n with
+  | 0 => 0
+  | S n => foo n
+  end.
+
+  Lemma using_foo:
+    forall (n:nat), foo n = 0 /\ bar n = 0.
+  Proof.
+    induction n ; split ; auto ;
+    destruct IHn ; auto.
+  Qed.
+
+End A.
+
+
+Module B.
+  
+  Module A := A.
+  Import A.
+
+End B.
+
+Module E.
+
+  Module B := B.
+  Import B.A.
+
+  (* Bug 1 *)
+  Lemma test_1:
+    forall (n:nat), foo n = 0.
+  Proof.
+    intros ; destruct n.
+    reflexivity.
+    specialize (A.using_foo (S n)) ; intros.
+    simpl in H.
+    simpl.
+    destruct H.
+    assumption.
+  Qed.
+
+End E.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2629.v b/test-suite/bugs/closed/shouldsucceed/2629.v
new file mode 100644
index 00000000..759cd3dd
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2629.v
@@ -0,0 +1,22 @@
+Class Join (t: Type) : Type := mkJoin {join: t -> t -> t -> Prop}.
+
+Class sepalg (t: Type) {JOIN: Join t} : Type :=
+  SepAlg   {
+   join_eq: forall {x y z z'}, join x y z -> join x y z' -> z = z';
+   join_assoc: forall {a b c d e}, join a b d -> join d c e ->
+                    {f : t & join b c f /\ join a f e};
+   join_com: forall {a b c}, join a b c -> join b a c;
+   join_canc: forall {a1 a2 b c}, join a1 b c -> join a2 b c -> a1=a2;
+
+   unit_for : t -> t -> Prop := fun e a => join e a a;
+   join_ex_units: forall a, {e : t & unit_for e a}
+}.
+
+Definition joins {A} `{Join A} (a b : A) : Prop :=
+ exists c, join a b c.
+
+Lemma join_joins {A} `{sepalg A}: forall {a b c},
+ join a b c -> joins a b.
+Proof.
+ firstorder.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2668.v b/test-suite/bugs/closed/shouldsucceed/2668.v
new file mode 100644
index 00000000..74c8fa34
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2668.v
@@ -0,0 +1,6 @@
+Require Import MSetPositive.
+Require Import MSetProperties.
+
+Module Pos := MSetPositive.PositiveSet.
+Module PPPP := MSetProperties.WPropertiesOn(Pos).
+Print Module PPPP.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2734.v b/test-suite/bugs/closed/shouldsucceed/2734.v
new file mode 100644
index 00000000..826361be
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2734.v
@@ -0,0 +1,15 @@
+Require Import Arith List.
+Require Import OrderedTypeEx.
+
+Module Adr.
+ Include Nat_as_OT.
+ Definition nat2t (i: nat) : t := i.
+End Adr.
+
+Inductive expr :=  Const: Adr.t -> expr.
+
+Inductive control := Go: expr ->  control.
+
+Definition program :=  (Adr.t * (control))%type.
+
+Fail Definition myprog : program := (Adr.nat2t 0,   Go (Adr.nat2t 0) ).
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2750.v b/test-suite/bugs/closed/shouldsucceed/2750.v
new file mode 100644
index 00000000..fc580f10
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2750.v
@@ -0,0 +1,23 @@
+
+Module Type ModWithRecord.
+
+  Record foo : Type :=
+  { A : nat
+  ; B : nat
+  }.
+End ModWithRecord.
+
+Module Test_ModWithRecord (M : ModWithRecord).
+
+  Definition test1 : M.foo :=
+    {| M.A := 0
+     ; M.B := 2
+     |}.
+
+  Module B := M.
+
+  Definition test2 : M.foo :=
+    {| M.A := 0
+     ; M.B := 2
+     |}.
+End Test_ModWithRecord.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2928.v b/test-suite/bugs/closed/shouldsucceed/2928.v
new file mode 100644
index 00000000..21e92ae2
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2928.v
@@ -0,0 +1,11 @@
+Class Equiv A := equiv: A -> A -> Prop.
+Infix "=" := equiv : type_scope.
+
+Class Associative {A} f `{Equiv A} := associativity x y z : f x (f y z) = f (f x y) z.
+
+Class SemiGroup A op `{Equiv A} := { sg_ass :>> Associative op }.
+
+Class SemiLattice A op `{Equiv A} :=
+    { semilattice_sg :>> SemiGroup A op
+    ; redundant : Associative op
+    }.
diff --git a/test-suite/bugs/closed/shouldsucceed/2983.v b/test-suite/bugs/closed/shouldsucceed/2983.v
new file mode 100644
index 00000000..15598352
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2983.v
@@ -0,0 +1,8 @@
+Module Type ModA.
+End ModA.
+Module Type ModB(A : ModA).
+End ModB.
+Module Foo(A : ModA)(B : ModB A).
+End Foo.
+
+Print Module Foo.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/2995.v b/test-suite/bugs/closed/shouldsucceed/2995.v
new file mode 100644
index 00000000..ba3acd08
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2995.v
@@ -0,0 +1,9 @@
+Module Type Interface.
+  Parameter error: nat.
+End Interface.
+
+Module Implementation <: Interface.
+  Definition t := bool.
+  Definition error: t := false.
+Fail End Implementation.
+(* A UserError here is expected, not an uncaught Not_found *)
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/3000.v b/test-suite/bugs/closed/shouldsucceed/3000.v
new file mode 100644
index 00000000..27de34ed
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3000.v
@@ -0,0 +1,2 @@
+Inductive t (t':Type) : Type := A | B.
+Definition d := match t with _ => 1 end. (* used to fail on list_chop *)
diff --git a/test-suite/bugs/closed/shouldsucceed/3004.v b/test-suite/bugs/closed/shouldsucceed/3004.v
new file mode 100644
index 00000000..896b1958
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3004.v
@@ -0,0 +1,7 @@
+Set Implicit Arguments.
+Unset Strict Implicit.
+Parameter (M : nat -> Type).
+Parameter (mp : forall (T1 T2 : Type) (f : T1 -> T2), list T1 -> list T2).
+
+Definition foo (s : list {n : nat & M n}) :=
+  let exT := existT in mp (fun x => projT1 x) s.
diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/shouldsucceed/3008.v
new file mode 100644
index 00000000..3f3a979a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3008.v
@@ -0,0 +1,29 @@
+Module Type Intf1.
+Parameter T : Type.
+Inductive a := A.
+End Intf1.
+
+Module Impl1 <: Intf1.
+Definition T := unit.
+Inductive a := A.
+End Impl1.
+
+Module Type Intf2
+  (Impl1 : Intf1).
+Parameter x : Impl1.A=Impl1.A -> Impl1.T.
+End Intf2.
+
+Module Type Intf3
+  (Impl1 : Intf1)
+  (Impl2 : Intf2(Impl1)).
+End Intf3.
+
+Fail Module Toto
+  (Impl1' : Intf1)
+  (Impl2 : Intf2(Impl1'))
+  (Impl3 : Intf3(Impl1)(Impl2)).
+(* A UserError is expected here, not an uncaught Not_found *)
+
+(* NB : the Inductive above and the A=A weren't in the initial test,
+   they are here only to force an access to the environment
+   (cf [Printer.qualid_of_global]) and check that this env is ok. *)
\ No newline at end of file
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index bca3b361..4f8de1dc 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -4,3 +4,7 @@ fun e : option L => match e with
                     | None => None
                     end
      : option L -> option L
+fun n : nat => let x := A n in ?12 ?15:T n
+     : forall n : nat, T n
+fun n : nat => ?20 ?23:T n
+     : forall n : nat, T n
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 968ea71a..2b564f48 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -12,3 +12,15 @@ Definition P (e:option L) :=
   end.
 
 Print P.
+
+(* Check that the heuristic to solve constraints is not artificially
+   dependent on the presence of a let-in, and in particular that the
+   second [_] below is not inferred to be n, as if obtained by
+   first-order unification with [T n] of the conclusion [T _] of the
+   type of the first [_]. *)
+
+(* Note: exact numbers of evars are not important... *)
+
+Inductive T (n:nat) : Type := A : T n.
+Check fun n (x:=A n:T n) => _ _ : T n.
+Check fun n => _ _ : T n.
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 5f8ed03d..0befe054 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -6,3 +6,11 @@ Fail remember nat as X.
 Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
 Fail remember nat as X.
 Abort.
+
+(* Testing Ltac interpretation of remember (was not working up to r16181) *)
+
+Goal (1 + 2 + 3 = 6).
+let name := fresh "fresh" in
+remember (1 + 2) as x eqn:name.
+rewrite fresh.
+Abort.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 5582438b..3dae9c70 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -646,4 +646,4 @@ End NZOrderProp.
 
 Module NZOrderedType (NZ : NZDecOrdSig')
  <: DecidableTypeFull <: OrderedTypeFull
- := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec.
+ := NZ <+ NZBaseProp <+ NZOrderProp NZ <+ Compare2EqBool <+ HasEqBool2Dec.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 3690b924..b9ab68ec 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -111,7 +111,7 @@ let mkFullInd ind n =
 
 let check_bool_is_defined () =
   try let _ = Global.type_of_global Coqlib.glob_bool in ()
-  with _ -> raise (UndefinedCst "bool")
+  with e when Errors.noncritical e -> raise (UndefinedCst "bool")
 
 let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
@@ -304,8 +304,9 @@ let destruct_ind c =
     try let u,v =  destApp c in
           let indc = destInd u in
             indc,v
-    with _-> let indc = destInd c in
-            indc,[||]
+    with e when Errors.noncritical e ->
+      let indc = destInd c in
+      indc,[||]
 
 (*
   In the following, avoid is the list of names to avoid.
@@ -329,8 +330,9 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q =
             else error ("Var "^(string_of_id s)^" seems unknown.")
       )
     in mkVar (find 1)
-  with _ -> (* if this happen then the args have to be already declared as a
-              Parameter*)
+  with e when Errors.noncritical e ->
+      (* if this happen then the args have to be already declared as a
+         Parameter*)
       (
         let mp,dir,lbl = repr_con (destConst v) in
           mkConst (make_con mp dir (mk_label (
@@ -376,8 +378,9 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
             else error ("Var "^(string_of_id s)^" seems unknown.")
       )
     in mkVar (find 1)
-  with _ -> (* if this happen then the args have to be already declared as a
-              Parameter*)
+  with e when Errors.noncritical e ->
+      (* if this happen then the args have to be already declared as a
+         Parameter*)
       (
         let mp,dir,lbl = repr_con (destConst v) in
           mkConst (make_con mp dir (mk_label (
@@ -394,7 +397,7 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
         else (
           let u,v = try  destruct_ind tt1
           (* trick so that the good sequence is returned*)
-                with _ -> ind,[||]
+                with e when Errors.noncritical e -> ind,[||]
           in if u = ind
              then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2)
              else (
@@ -427,17 +430,19 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
     | ([],[]) -> []
     | _ -> error "Both side of the equality must have the same arity."
   in
-  let (ind1,ca1) = try destApp lft with
-    _ -> error "replace failed."
-  and (ind2,ca2) = try destApp rgt with
-    _ -> error "replace failed."
+  let (ind1,ca1) =
+    try destApp lft with e when Errors.noncritical e -> error "replace failed."
+  and (ind2,ca2) =
+    try destApp rgt with e when Errors.noncritical e -> error "replace failed."
   in
-  let (sp1,i1) = try destInd ind1 with
-    _ -> (try fst (destConstruct ind1) with _ ->
-                error "The expected type is an inductive one.")
-  and (sp2,i2) = try destInd ind2 with
-    _ -> (try fst (destConstruct ind2)  with _ ->
-                error "The expected type is an inductive one.")
+  let (sp1,i1) =
+    try destInd ind1 with e when Errors.noncritical e ->
+      try fst (destConstruct ind1) with e when Errors.noncritical e ->
+        error "The expected type is an inductive one."
+  and (sp2,i2) =
+    try destInd ind2 with e when Errors.noncritical e ->
+      try fst (destConstruct ind2) with e when Errors.noncritical e ->
+        error "The expected type is an inductive one."
   in
     if (sp1 <> sp2) || (i1 <> i2)
       then (error "Eq should be on the same type")
@@ -714,7 +719,8 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind
 (* Decidable equality *)
 
 let check_not_is_defined () =
-  try ignore (Coqlib.build_coq_not ()) with _ -> raise (UndefinedCst "not")
+  try ignore (Coqlib.build_coq_not ())
+  with e when Errors.noncritical e -> raise (UndefinedCst "not")
 
 (* {n=m}+{n<>m}  part  *)
 let compute_dec_goal ind lnamesparrec nparrec =
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 10709abc..f43fc505 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -204,7 +204,8 @@ let declare_class_instance gr ctx params =
     (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
   Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst));
   new_instance_message ident typ def
-  with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str"  "++Errors.print e)
+  with e when Errors.noncritical e ->
+    msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str"  "++Errors.print e)
 
 let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t;
   match kind_of_term t with
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
index 912d694e..f444fc2d 100644
--- a/toplevel/backtrack.ml
+++ b/toplevel/backtrack.ml
@@ -96,7 +96,9 @@ let mark_command ast =
   Stack.push
     { label = Lib.current_command_label ();
       nproofs = List.length (Pfedit.get_all_proof_names ());
-      prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None);
+      prfname =
+        (try Some (Pfedit.get_current_proof_name ())
+         with Proof_global.NoCurrentProof -> None);
       prfdepth = max 0 (Pfedit.current_proof_depth ());
       reachable = true;
       ngoals = get_ngoals ();
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 6914b8f0..de4d1ab1 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -37,7 +37,10 @@ let set_typeclass_transparency c local b =
 let _ =
   Typeclasses.register_add_instance_hint
     (fun inst local pri ->
-     let path = try Auto.PathHints [global_of_constr inst] with _ -> Auto.PathAny in
+     let path =
+       try Auto.PathHints [global_of_constr inst]
+       with e when Errors.noncritical e -> Auto.PathAny
+     in
       Flags.silently (fun () ->
 	Auto.add_hints local [typeclasses_db]
 	  (Auto.HintsResolveEntry
@@ -300,8 +303,10 @@ let context l =
   let fullctx = Evarutil.nf_rel_context_evar !evars fullctx in
   let ce t = Evarutil.check_evars env Evd.empty !evars t in
   List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
-  let ctx = try named_of_rel_context fullctx with _ ->
-    error "Anonymous variables not allowed in contexts."
+  let ctx =
+    try named_of_rel_context fullctx
+    with e when Errors.noncritical e ->
+      error "Anonymous variables not allowed in contexts."
   in
   let fn (id, _, t) =
     if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 66a9516a..8f954573 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -46,9 +46,9 @@ let load_rcfile() =
 	  mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
 			 " found. Skipping rcfile loading."))
 	*)
-    with e ->
+    with reraise ->
       (msgnl (str"Load of rcfile failed.");
-       raise e)
+       raise reraise)
   else
     Flags.if_verbose msgnl (str"Skipping rcfile loading.")
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index df388d1d..adbdb31b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -24,7 +24,8 @@ let get_version_date () =
     let ver = input_line ch in
     let rev = input_line ch in
       (ver,rev)
-  with _ -> (Coq_config.version,Coq_config.date)
+  with e when Errors.noncritical e ->
+    (Coq_config.version,Coq_config.date)
 
 let print_header () =
   let (ver,rev) = (get_version_date ()) in
@@ -310,7 +311,7 @@ let parse_args arglist =
 	with Stream.Failure ->
 	  msgnl (Errors.print e); exit 1
       end
-    | e -> begin msgnl (Errors.print e); exit 1 end
+    | any -> begin msgnl (Errors.print any); exit 1 end
 
 let init arglist =
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
@@ -344,10 +345,10 @@ let init arglist =
       load_vernacular ();
       compile_files ();
       outputstate ()
-    with e ->
+    with any ->
       flush_all();
       if not !batch_mode then message "Error during initialization:";
-      msgnl (Toplevel.print_toplevel_error e);
+      msgnl (Toplevel.print_toplevel_error any);
       exit 1
   end;
   if !batch_mode then
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index e7b5a0f2..f550df16 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -28,6 +28,8 @@ open Logic
 open Printer
 open Glob_term
 open Evd
+open Libnames
+open Declarations
 
 let pr_lconstr c = quote (pr_lconstr c)
 let pr_lconstr_env e c = quote (pr_lconstr_env e c)
@@ -307,7 +309,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
       let fixenv = make_all_name_different fixenv in
       let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in
 	str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
-    with _ -> mt ())
+    with e when Errors.noncritical e -> mt ())
 
 let explain_ill_typed_rec_body env sigma i names vdefj vargs =
   let vdefj = jv_nf_evar sigma vdefj in
@@ -542,8 +544,11 @@ let explain_not_match_error = function
     str "types given to " ++ str (string_of_id id) ++ str " differ"
   | NotConvertibleBodyField ->
     str "the body of definitions differs"
-  | NotConvertibleTypeField ->
-    str "types differ"
+  | NotConvertibleTypeField (env, typ1, typ2) ->
+    str "expected type" ++ spc ()  ++
+    quote (Printer.safe_pr_lconstr_env env typ2) ++ spc () ++
+    str "but found type" ++ spc () ++
+    quote (Printer.safe_pr_lconstr_env env typ1)
   | NotSameConstructorNamesField ->
     str "constructor names differ"
   | NotSameInductiveNameInBlockField ->
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 28f97dc8..6937eeb8 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -89,8 +89,8 @@ let abstract_eval_call handler c =
       | Quit -> Obj.magic (handler.quit () : unit)
       | About -> Obj.magic (handler.about () : coq_info)
     in Good res
-  with e ->
-    let (l, str) = handler.handle_exn e in
+  with any ->
+    let (l, str) = handler.handle_exn any in
     Fail (l,str)
 
 (** * XML data marshalling *)
@@ -275,7 +275,7 @@ let to_value f = function
         let loc_s = int_of_string (List.assoc "loc_s" attrs) in
         let loc_e = int_of_string (List.assoc "loc_e" attrs) in
         Some (loc_s, loc_e)
-      with _ -> None
+      with e when e <> Sys.Break -> None
     in
     let msg = raw_string l in
     Fail (loc, msg)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index d67b272e..6e9a0ee0 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -237,7 +237,7 @@ let status () =
   in
   let proof =
     try Some (Names.string_of_id (Proof_global.get_current_proof_name ()))
-    with _ -> None
+    with Proof_global.NoCurrentProof -> None
   in
   let allproofs =
     let l = Proof_global.get_all_proof_names () in
@@ -259,7 +259,8 @@ let search flags =
   | (Interface.Name_Pattern s, b) :: l ->
     let regexp =
       try Str.regexp s
-      with _ -> Util.error ("Invalid regexp: " ^ s)
+      with e when Errors.noncritical e ->
+        Util.error ("Invalid regexp: " ^ s)
     in
     extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
   | (Interface.Type_Pattern s, b) :: l ->
@@ -454,12 +455,12 @@ let loop () =
       Xml_utils.print_xml !orig_stdout xml_answer;
       flush !orig_stdout
     done
-  with e ->
-    let msg = Printexc.to_string e in
+  with any ->
+    let msg = Printexc.to_string any in
     let r = "Fatal exception in coqtop:\n" ^ msg in
     pr_debug ("==> " ^ r);
     (try
       Xml_utils.print_xml !orig_stdout (fail r);
       flush !orig_stdout
-    with _ -> ());
+    with any -> ());
     exit 1
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 9f1a0218..77cfa6fa 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -86,8 +86,9 @@ let scheme_object_table =
   (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
 
 let declare_scheme_object s aux f =
-  (try check_ident ("ind"^s) with _ ->
-    error ("Illegal induction scheme suffix: "^s));
+  (try check_ident ("ind"^s)
+   with e when Errors.noncritical e ->
+     error ("Illegal induction scheme suffix: "^s));
   let key = if aux = "" then s else aux in
   try
     let _ = Hashtbl.find scheme_object_table key in
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index fa6885af..e30404e1 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -159,7 +159,7 @@ let try_declare_scheme what f internal names kn =
 	  (strbrk "Required constant " ++ str s ++ str " undefined.")
     | AlreadyDeclared msg ->
         alarm what internal (msg ++ str ".")
-    | _ -> 
+    | e when Errors.noncritical e ->
 	alarm what internal
 	  (str "Unknown exception during scheme creation.")
 
@@ -245,7 +245,8 @@ let try_declare_eq_decidability kn =
 
 let declare_eq_decidability = declare_eq_decidability_scheme_with []
 
-let ignore_error f x = try ignore (f x) with _ -> ()
+let ignore_error f x =
+  try ignore (f x) with e when Errors.noncritical e -> ()
 
 let declare_rewriting_schemes ind =
   if Hipattern.is_inductive_equality ind then begin
@@ -266,7 +267,7 @@ let declare_congr_scheme ind =
   if Hipattern.is_equality_type (mkInd ind) then begin
     if
       try Coqlib.check_required_library Coqlib.logic_module_name; true
-      with _ -> false
+      with e when Errors.noncritical e -> false
     then
       ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind)
     else
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index d6ab44c6..30f07fed 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -229,23 +229,32 @@ let get_proof opacity =
   id,{const with const_entry_opaque = opacity},do_guard,persistence,hook
 
 let save_named opacity =
-  let id,const,do_guard,persistence,hook = get_proof opacity in
-  save id const do_guard persistence hook
+  let p = Proof_global.give_me_the_proof () in
+  Proof.transaction p begin fun () ->
+    let id,const,do_guard,persistence,hook = get_proof opacity in
+    save id const do_guard persistence hook
+  end
 
 let check_anonymity id save_ident =
   if atompart_of_id id <> string_of_id (default_thm_id) then
     error "This command can only be used for unnamed theorem."
 
 let save_anonymous opacity save_ident =
-  let id,const,do_guard,persistence,hook = get_proof opacity in
-  check_anonymity id save_ident;
-  save save_ident const do_guard persistence hook
+  let p = Proof_global.give_me_the_proof () in
+  Proof.transaction p begin fun () ->
+    let id,const,do_guard,persistence,hook = get_proof opacity in
+    check_anonymity id save_ident;
+    save save_ident const do_guard persistence hook
+  end
 
 let save_anonymous_with_strength kind opacity save_ident =
-  let id,const,do_guard,_,hook = get_proof opacity in
-  check_anonymity id save_ident;
-  (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const do_guard (Global, Proof kind) hook
+  let p = Proof_global.give_me_the_proof () in
+  Proof.transaction p begin fun () ->
+    let id,const,do_guard,_,hook = get_proof opacity in
+    check_anonymity id save_ident;
+    (* we consider that non opaque behaves as local for discharge *)
+    save save_ident const do_guard (Global, Proof kind) hook
+  end
 
 (* Starting a goal *)
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 775a3af4..006dc5ec 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -237,7 +237,7 @@ let parse_format (loc,str) =
       | _ -> error "Box closed without being opened in format."
     else
       error "Empty format."
-  with e ->
+  with e when Errors.noncritical e ->
     Loc.raise loc e
 
 (***********************)
@@ -277,6 +277,9 @@ let split_notation_string str =
 
 let out_nt = function NonTerminal x -> x | _ -> assert false
 
+let msg_expected_form_of_recursive_notation =
+  "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"."
+
 let rec find_pattern nt xl = function
   | Break n as x :: l, Break n' :: l' when n=n' ->
       find_pattern nt (x::xl) (l,l')
@@ -289,13 +292,14 @@ let rec find_pattern nt xl = function
   | _, Break s :: _ | Break s :: _, _ ->
       error ("A break occurs on one side of \"..\" but not on the other side.")
   | _, [] ->
-      error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
+      error msg_expected_form_of_recursive_notation
   | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
       anomaly "Only Terminal or Break expected on left, non-SProdList on right"
 
 let rec interp_list_parser hd = function
   | [] -> [], List.rev hd
   | NonTerminal id :: tl when id = ldots_var ->
+      if hd = [] then error msg_expected_form_of_recursive_notation;
       let hd = List.rev hd in
       let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
       let xyl,tl'' = interp_list_parser [] tl' in
@@ -337,7 +341,8 @@ let rec raw_analyze_notation_tokens = function
 let is_numeral symbs =
   match List.filter (function Break _ -> false | _ -> true) symbs with
   | ([Terminal "-"; Terminal x] | [Terminal x]) ->
-      (try let _ = Bigint.of_string x in true with _ -> false)
+      (try let _ = Bigint.of_string x in true
+       with e when Errors.noncritical e -> false)
   | _ ->
       false
 
@@ -995,7 +1000,7 @@ let inNotation : notation_obj -> obj =
 let with_lib_stk_protection f x =
   let fs = Lib.freeze () in
   try let a = f x in Lib.unfreeze fs; a
-  with e -> Lib.unfreeze fs; raise e
+  with reraise -> Lib.unfreeze fs; raise reraise
 
 let with_syntax_protection f x =
   with_lib_stk_protection
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 2059ca60..f08308d3 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -92,8 +92,9 @@ let dir_ml_load s =
       (try t.load_obj s
        with
        | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u
-       | _ -> errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
-                str s ++ str" to Coq code."))
+       | e when Errors.noncritical e ->
+         errorlabstrm "Mltop.load_object"
+           (str"Cannot link ml-object " ++ str s ++ str" to Coq code."))
 (* TO DO: .cma loading without toplevel *)
     | WithoutTop ->
       IFDEF HasDynlink THEN
@@ -142,7 +143,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
 
 let convert_string d =
   try Names.id_of_string d
-  with _ ->
+  with e when Errors.noncritical e ->
     if_warn msg_warning
       (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
     flush_all ();
@@ -269,9 +270,9 @@ let if_verbose_load verb f name fname =
     try
       f name fname;
       msgnl (str (info^" done]"));
-    with e ->
+    with reraise ->
       msgnl (str (info^" failed]"));
-      raise e
+      raise reraise
 
 (** Load a module for the first time (i.e. dynlink it)
     or simulate its reload (i.e. doing nothing except maybe
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 3e182689..19d696a1 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -137,7 +137,7 @@ let pattern_filter pat _ a c =
   try
     try
       is_matching pat (head c)
-    with _ ->
+    with e when Errors.noncritical e ->
       is_matching
 	pat (head (Typing.type_of (Global.env()) Evd.empty c))
     with UserError _ ->
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index d5321623..cc659e36 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -180,7 +180,7 @@ let print_location_in_file s inlibrary fname loc =
            str", line " ++ int line ++ str", characters " ++
            Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++
         fnl ()
-      with e ->
+      with e when Errors.noncritical e ->
         (close_in ic;
          hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
 
@@ -208,7 +208,7 @@ let valid_buffer_loc ib dloc loc =
 let make_prompt () =
   try
     (Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < "
-  with _ ->
+  with Proof_global.NoCurrentProof ->
     "Coq < "
 
 (*let build_pending_list l =
@@ -340,7 +340,7 @@ let process_error = function
 	  discard_to_dot (); e
 	with
           | End_of_input -> End_of_input
-          | de -> if is_pervasive_exn de then de else e
+          | any -> if is_pervasive_exn any then any else e
 
 (* do_vernac reads and executes a toplevel phrase, and print error
    messages when an exception is raised, except for the following:
@@ -354,8 +354,8 @@ let do_vernac () =
   begin
     try
       raw_do_vernac top_buffer.tokens
-    with e ->
-      msgnl (print_toplevel_error (process_error e))
+    with any ->
+      msgnl (print_toplevel_error (process_error any))
   end;
   flush_all()
 
@@ -374,6 +374,6 @@ let rec loop () =
     | Vernacexpr.Drop -> ()
     | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0
     | Vernacexpr.Quit -> exit 0
-    | e ->
+    | any ->
 	msgerrnl (str"Anomaly. Please report.");
 	loop ()
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 3314e82c..ed8e215f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -156,7 +156,7 @@ let close_input in_chan (_,verb) =
     match verb with
       | Some verb_ch -> close_in verb_ch
       | _ -> ()
-  with _ -> ()
+  with e when Errors.noncritical e -> ()
 
 let verbose_phrase verbch loc =
   let loc = unloc loc in
@@ -232,13 +232,13 @@ let rec vernac_com interpfun checknav (loc,com) =
               Lexer.restore_com_state cs;
               Pp.comments := cl;
               Dumpglob.coqdoc_unfreeze cds
-	    with e ->
+	    with reraise ->
 	      if !Flags.beautify_file then close_out !chan_beautify;
               chan_beautify := ch;
               Lexer.restore_com_state cs;
               Pp.comments := cl;
               Dumpglob.coqdoc_unfreeze cds;
-	      raise e
+	      raise reraise
 	  end
 
     | VernacList l -> List.iter (fun (_,v) -> interp v) l
@@ -250,7 +250,7 @@ let rec vernac_com interpfun checknav (loc,com) =
 	  (* If the command actually works, ignore its effects on the state *)
 	  States.with_state_protection
 	    (fun v -> interp v; raise HasNotFailed) v
-	with e -> match real_error e with
+	with e when Errors.noncritical e -> match real_error e with
 	  | HasNotFailed ->
 	      errorlabstrm "Fail" (str "The command has not failed !")
 	  | e ->
@@ -278,16 +278,16 @@ let rec vernac_com interpfun checknav (loc,com) =
             States.with_heavy_rollback interpfun
               Cerrors.process_vernac_interp_error v;
 	    restore_timeout psh
-	  with e -> restore_timeout psh; raise e
+	  with reraise -> restore_timeout psh; raise reraise
   in
     try
       checknav loc com;
       current_timeout := !default_timeout;
       if do_beautify () then pr_new_syntax loc (Some com);
       interp com
-    with e ->
+    with any ->
       Format.set_formatter_out_channel stdout;
-      raise (DuringCommandInterp (loc, e))
+      raise (DuringCommandInterp (loc, any))
 
 and read_vernac_file verbosely s =
   Flags.make_warn verbosely;
@@ -316,13 +316,13 @@ and read_vernac_file verbosely s =
       end_inner_command (snd loc_ast);
       pp_flush ()
     done
-  with e ->   (* whatever the exception *)
+  with reraise ->   (* whatever the exception *)
     Format.set_formatter_out_channel stdout;
     close_input in_chan input;    (* we must close the file first *)
-    match real_error e with
+    match real_error reraise with
       | End_of_input ->
           if do_beautify () then pr_new_syntax (make_loc (max_int,max_int)) None
-      | _ -> raise_with_file fname e
+      | _ -> raise_with_file fname reraise
 
 (** [eval_expr : ?preserving:bool -> Pp.loc * Vernacexpr.vernac_expr -> unit]
    It executes one vernacular command. By default the command is
@@ -359,9 +359,9 @@ let load_vernac verb file =
     Lib.mark_end_of_command (); (* in case we're still in coqtop init *)
     read_vernac_file verb file;
     if !Flags.beautify_file then close_out !chan_beautify;
-  with e ->
+  with reraise ->
     if !Flags.beautify_file then close_out !chan_beautify;
-    raise_with_file file e
+    raise_with_file file reraise
 
 (* Compile a vernac file (f is assumed without .v suffix) *)
 let compile verbosely f =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6618b695..75efe139 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -295,7 +295,7 @@ let dump_universes_gen g s =
     close ();
     msgnl (str ("Universes written to file \""^s^"\"."))
   with
-      e -> close (); raise e
+      reraise -> close (); raise reraise
 
 let dump_universes sorted s =
   let g = Global.universes () in
@@ -331,7 +331,7 @@ let msg_notfound_library loc qid = function
 let print_located_library r =
   let (loc,qid) = qualid_of_reference r in
   try msg_found_library (Library.locate_qualified_library false qid)
-  with e -> msg_notfound_library loc qid e
+  with e when Errors.noncritical e -> msg_notfound_library loc qid e
 
 let print_located_module r =
   let (loc,qid) = qualid_of_reference r in
@@ -364,7 +364,7 @@ let dump_global r =
   try
     let gr = Smartlocate.smart_global r in
     Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr
-  with _ -> ()
+  with e when Errors.noncritical e -> ()
 (**********)
 (* Syntax *)
 
@@ -388,6 +388,7 @@ let vernac_notation = Metasyntax.add_notation
 (* Gallina *)
 
 let start_proof_and_print k l hook =
+  check_locality (); (* early check, cf #2975 *)
   start_proof_com k l hook;
   print_subgoals ();
   if !pcoq <> None then (Option.get !pcoq).start_proof ()
@@ -910,7 +911,9 @@ let vernac_declare_arguments local r l nargs flags =
     | None -> None
     | Some (o, k) -> 
         try Some(ignore(Notation.find_scope k); k)
-        with _ -> Some (Notation.find_delimiters_scope o k)) scopes in
+        with e when Errors.noncritical e ->
+          Some (Notation.find_delimiters_scope o k)) scopes
+  in
   let some_scopes_specified = List.exists ((<>) None) scopes in
   let rargs =
     Util.list_map_filter (function (n, true) -> Some n | _ -> None)
@@ -1417,7 +1420,7 @@ let vernac_reset_name id =
 	let gr = Smartlocate.global_with_alias (Ident id) in
 	Dumpglob.add_glob (fst id) gr;
 	true
-      with _ -> false in
+      with e when Errors.noncritical e -> false in
 
     if not globalized then begin
        try begin match Lib.find_opening_node (snd id) with
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index c4cc4ae5..a1b76d3d 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -60,7 +60,7 @@ let call (opn,converted_args) =
     hunk()
   with
     | Drop -> raise Drop
-    | e ->
+    | reraise ->
         if !Flags.debug then
 	  msgnl (str"Vernac Interpreter " ++ str !loc);
-        raise e
+        raise reraise