summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml44
-rw-r--r--toplevel/autoinstance.ml3
-rw-r--r--toplevel/backtrack.ml4
-rw-r--r--toplevel/classes.ml11
-rw-r--r--toplevel/coqinit.ml4
-rw-r--r--toplevel/coqtop.ml9
-rw-r--r--toplevel/himsg.ml11
-rw-r--r--toplevel/ide_intf.ml6
-rw-r--r--toplevel/ide_slave.ml11
-rw-r--r--toplevel/ind_tables.ml5
-rw-r--r--toplevel/indschemes.ml7
-rw-r--r--toplevel/lemmas.ml27
-rw-r--r--toplevel/metasyntax.ml13
-rw-r--r--toplevel/mltop.ml411
-rw-r--r--toplevel/search.ml2
-rw-r--r--toplevel/toplevel.ml12
-rw-r--r--toplevel/vernac.ml24
-rw-r--r--toplevel/vernacentries.ml13
-rw-r--r--toplevel/vernacinterp.ml4
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-30 09:38:17 +0000