Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

19 files changed, 131 insertions, 90 deletions

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