aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml43
-rw-r--r--lib/bigint.mli2
-rw-r--r--printing/printer.ml3
-rw-r--r--printing/printmod.ml10
-rw-r--r--scripts/coqmktop.ml2
-rw-r--r--tactics/class_tactics.ml48
-rw-r--r--tactics/eauto.ml43
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/hipattern.ml45
-rw-r--r--tactics/rewrite.ml418
-rw-r--r--tools/coq_tex.ml6
-rw-r--r--toplevel/auto_ind_decl.ml28
-rw-r--r--toplevel/autoinstance.ml4
-rw-r--r--toplevel/backtrack.ml4
-rw-r--r--toplevel/classes.ml6
-rw-r--r--toplevel/command.ml4
-rw-r--r--toplevel/coqinit.ml6
-rw-r--r--toplevel/coqtop.ml16
-rw-r--r--toplevel/himsg.ml2
-rw-r--r--toplevel/ide_slave.ml6
-rw-r--r--toplevel/ind_tables.ml2
-rw-r--r--toplevel/indschemes.ml7
-rw-r--r--toplevel/metasyntax.ml10
-rw-r--r--toplevel/mltop.ml9
-rw-r--r--toplevel/obligations.ml17
-rw-r--r--toplevel/search.ml5
-rw-r--r--toplevel/toplevel.ml12
-rw-r--r--toplevel/vernac.ml31
-rw-r--r--toplevel/vernacentries.ml41
-rw-r--r--toplevel/vernacinterp.ml6
30 files changed, 156 insertions, 122 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 7aacfa24e..0959bfcc1 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -140,7 +140,8 @@ 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/lib/bigint.mli b/lib/bigint.mli
index 8b61a1fb6..8c2bf5c48 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -11,7 +11,7 @@
type bigint
val of_string : string -> bigint
-(** May a Failure just as [int_of_string] on non-numerical strings *)
+(** May raise a Failure just as [int_of_string] on non-numerical strings *)
val to_string : bigint -> string
diff --git a/printing/printer.ml b/printing/printer.ml
index e73ccfb35..ea6e79876 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -591,7 +591,8 @@ let pr_assumptionset env s =
str (string_of_mp mp ^ "." ^ Label.to_string 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 fold t typ accu =
let (v, a, o, tr) = accu in
diff --git a/printing/printmod.ml b/printing/printmod.ml
index fd9b1f200..a3dab2806 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -157,7 +157,8 @@ 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 (MBId.to_id mbid))::locals
in
- (try Declaremods.process_module_seb_binding mbid seb1 with _ -> ());
+ (try Declaremods.process_module_seb_binding mbid seb1
+ with e when Errors.noncritical e -> ());
hov 2 (str "Funsig" ++ spc () ++ str "(" ++
pr_id (MBId.to_id mbid) ++ str ":" ++
print_modtype env mp1 locals seb1 ++
@@ -191,7 +192,8 @@ 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 (MBId.to_id mbid))::locals in
- (try Declaremods.process_module_seb_binding mbid typ with _ -> ());
+ (try Declaremods.process_module_seb_binding mbid typ
+ with e when Errors.noncritical e -> ());
hov 2 (str "Functor" ++ spc() ++ str"(" ++ pr_id(MBId.to_id mbid) ++
str ":" ++ print_modtype env mp' locals typ ++
str ")" ++ spc () ++ print_modexpr env' mp locals' mexpr)
@@ -244,7 +246,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 =
@@ -255,5 +257,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/scripts/coqmktop.ml b/scripts/coqmktop.ml
index a9ec68220..88156f6fa 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -316,6 +316,6 @@ let main () =
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/class_tactics.ml4 b/tactics/class_tactics.ml4
index 329be18eb..123b2a2ef 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -690,7 +690,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
@@ -780,7 +780,11 @@ 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 caebb76d4..1be29aefe 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -197,7 +197,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/extratactics.ml4 b/tactics/extratactics.ml4
index 7a8cccc6d..a8188d582 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -611,7 +611,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 fadc50661..286aa9492 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -366,7 +366,10 @@ let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
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 (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 20bcb84a7..a3006e99c 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -118,7 +118,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 _ =
@@ -218,7 +218,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
@@ -1040,7 +1040,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
@@ -1048,7 +1049,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 ->
@@ -1056,7 +1057,8 @@ module Strategies =
let sigma, c = Pretyping.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
@@ -1064,7 +1066,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
@@ -1306,7 +1308,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
let newtactic_init_setoid () =
try init_setoid (); Proofview.tclUNIT ()
- with e -> Proofview.tclZERO e
+ with e when Errors.noncritical e -> Proofview.tclZERO e
let tactic_init_setoid () =
init_setoid (); tclIDTAC
@@ -1979,7 +1981,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 ->
let e = Errors.push e in
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 87db336d9..c19a9c3f1 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -209,7 +209,7 @@ let insert texfile coq_output result =
(* Process of one TeX file *)
-let rm f = try Sys.remove f with _ -> ()
+let rm f = try Sys.remove f with any -> ()
let one_file texfile =
let inputv = Filename.temp_file "coq_tex" ".v" in
@@ -233,9 +233,9 @@ let one_file texfile =
insert texfile coq_output result;
(* 4. clean up *)
rm inputv; rm coq_output
- with e -> begin
+ with reraise -> begin
rm inputv; rm coq_output;
- raise e
+ raise reraise
end
(* Parsing of the command line, check of the Coq command and process
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 31d03ff0c..3ba32da3c 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -424,21 +424,23 @@ 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
- DestKO -> error "replace failed."
- and (ind2,ca2) = try destApp rgt with
- DestKO -> error "replace failed."
+ let (ind1,ca1) =
+ try destApp lft with DestKO -> error "replace failed."
+ and (ind2,ca2) =
+ try destApp rgt with DestKO -> error "replace failed."
in
- let (sp1,i1) = try destInd ind1 with
- DestKO -> (try fst (destConstruct ind1) with _ ->
- error "The expected type is an inductive one.")
- and (sp2,i2) = try destInd ind2 with
- DestKO -> (try fst (destConstruct ind2) with _ ->
- error "The expected type is an inductive one.")
+ let (sp1,i1) =
+ try destInd ind1 with DestKO ->
+ try fst (destConstruct ind1) with DestKO ->
+ error "The expected type is an inductive one."
+ and (sp2,i2) =
+ try destInd ind2 with DestKO ->
+ try fst (destConstruct ind2) with DestKO ->
+ error "The expected type is an inductive one."
in
- if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
- then (error "Eq should be on the same type")
- else (aux (Array.to_list ca1) (Array.to_list ca2))
+ if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
+ then error "Eq should be on the same type"
+ else aux (Array.to_list ca1) (Array.to_list ca2)
(*
create, from a list of ids [i1,i2,...,in] the list
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 97d655da5..955b42700 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -206,7 +206,9 @@ 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 -> msg_info (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Errors.print e)
+ with e when Errors.noncritical e ->
+ msg_info (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 2d1e1c6a3..1954d1682 100644
--- a/toplevel/backtrack.ml
+++ b/toplevel/backtrack.ml
@@ -97,7 +97,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 8bb7c859f..915ab9d4c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -321,8 +321,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
let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in
- 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 status (id, _, t) =
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
diff --git a/toplevel/command.ml b/toplevel/command.ml
index a98daf709..0b2e6b352 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -621,7 +621,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_evars isevars binders_env measure relargty in
let wf_rel, wf_rel_fun, measure_fn =
@@ -751,7 +751,7 @@ let interp_recursive isfix fixl notations =
let sort = Retyping.get_type_of env !evdref t in
let fixprot =
try mkApp (delayed_force fix_proto, [|sort; t|])
- with e -> t
+ with e when Errors.noncritical e -> t
in
(id,None,fixprot) :: env'
else (id,None,t) :: env')
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 046bf7812..dfe576a69 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -50,10 +50,10 @@ let load_rcfile() =
mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
" found. Skipping rcfile loading."))
*)
- with e ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
let () = msg_info (str"Load of rcfile failed.") in
- raise e
+ raise reraise
else
Flags.if_verbose msg_info (str"Skipping rcfile loading.")
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index fadf301b8..386567dee 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -28,7 +28,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
@@ -351,7 +352,7 @@ let parse_args arglist =
| UserError(_, s) as e ->
if is_empty s then exit 1
else fatal_error (Errors.print e)
- | e -> fatal_error (Errors.print e)
+ | any -> fatal_error (Errors.print any)
let init arglist =
init_gc ();
@@ -386,12 +387,13 @@ let init arglist =
load_vernacular ();
compile_files ();
outputstate ()
- with e ->
+ with any ->
flush_all();
- if not !batch_mode then
- fatal_error (str "Error during initialization:" ++ fnl () ++ Toplevel.print_toplevel_error e)
- else
- fatal_error (Toplevel.print_toplevel_error e)
+ let msg =
+ if !batch_mode then mt ()
+ else str "Error during initialization:" ++ fnl ()
+ in
+ fatal_error (msg ++ Toplevel.print_toplevel_error any)
end;
if !batch_mode then
(flush_all();
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4c2e06331..87df8a055 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -350,7 +350,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 = Evarutil.jv_nf_evar sigma vdefj in
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index fcec3a128..205890977 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -240,7 +240,7 @@ let status () =
in
let proof =
try Some (Names.Id.to_string (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
@@ -376,8 +376,8 @@ let loop () =
| Serialize.Marshal_error ->
pr_debug "Incorrect query.";
exit 1
- | e ->
- pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string e);
+ | any ->
+ pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any);
exit 1
done;
pr_debug "Exiting gracefully.";
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 7cf60b7ff..5acbb78b7 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -87,7 +87,7 @@ let scheme_object_table =
(Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
let declare_scheme_object s aux f =
- (try Id.check ("ind"^s) with _ ->
+ (try Id.check ("ind"^s) with UserError _ ->
error ("Illegal induction scheme suffix: "^s));
let key = if String.is_empty aux then s else aux in
try
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 3aaf49548..616430007 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -169,7 +169,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.")
@@ -255,7 +255,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
@@ -276,7 +277,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/metasyntax.ml b/toplevel/metasyntax.ml
index a1b9574d8..bfb481475 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -266,7 +266,7 @@ let parse_format ((loc, str) : lstring) =
| _ -> error "Box closed without being opened in format."
else
error "Empty format."
- with e ->
+ with e when Errors.noncritical e ->
let e = Errors.push e in
Loc.raise loc e
@@ -371,7 +371,7 @@ 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 Failure _ -> false)
| _ ->
false
@@ -1074,10 +1074,10 @@ 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 ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
let () = Lib.unfreeze fs in
- raise e
+ raise reraise
let with_syntax_protection f x =
with_lib_stk_protection
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index e5e4ff599..e0daf53f1 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -117,11 +117,10 @@ let dir_ml_load s =
| WithTop t ->
(try t.load_obj s
with
- | e ->
+ | e when Errors.noncritical e ->
let e = Errors.push e in
match e with
| (UserError _ | Failure _ | Not_found as u) -> raise u
- | u when is_anomaly u -> raise u
| exc ->
let msg = report_on_load_obj_error exc in
errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
@@ -164,7 +163,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
let convert_string d =
try Names.Id.of_string d
- with _ ->
+ with UserError _ ->
if_warn msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
raise Exit
@@ -293,9 +292,9 @@ let if_verbose_load verb f name fname =
try
f name fname;
msg_info (str (info^" done]"));
- with e ->
+ with reraise ->
msg_info (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/obligations.ml b/toplevel/obligations.ml
index b52a7b2cd..a48e32bb2 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -380,7 +380,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 []
@@ -735,10 +735,10 @@ let solve_by_tac evi t =
Inductiveops.control_only_guard (Global.env ())
const.Entries.const_entry_body;
const.Entries.const_entry_body
- with e ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
Pfedit.delete_current_proof();
- raise e
+ raise reraise
let rec solve_obligation prg num tac =
let user_num = succ num in
@@ -771,8 +771,10 @@ let rec solve_obligation prg num tac =
in
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))
+ let res =
+ try update_obls prg obls (pred rem)
+ with e when Errors.noncritical e ->
+ pperror (Errors.print (Cerrors.process_vernac_interp_error e))
in
match res with
| Remain n when n > 0 ->
@@ -819,13 +821,12 @@ and solve_obligation_by_tac prg obls i tac =
obls.(i) <- declare_obligation prg obl t;
true
else false
- with e ->
+ with e when Errors.noncritical e ->
let e = Errors.push e in
match e with
| Proof_type.LtacLocated (_, _, Refiner.FailError (_, s))
| Refiner.FailError (_, s) ->
user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
- | e when Errors.is_anomaly e -> raise e
| e -> false
and solve_prg_obligations prg ?oblset tac =
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 80ffa36fb..c492f077d 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -141,7 +141,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 _ ->
@@ -264,7 +264,8 @@ let interface_search flags =
| (Interface.Name_Pattern s, b) :: l ->
let regexp =
try Str.regexp s
- with _ -> Errors.error ("Invalid regexp: " ^ s)
+ with e when Errors.noncritical e ->
+ Errors.error ("Invalid regexp: " ^ s)
in
extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
| (Interface.Type_Pattern s, b) :: l ->
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 19cb22c13..93a1c21f8 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -178,7 +178,7 @@ let print_location_in_file s inlibrary fname loc =
str", line " ++ int line ++ str", characters " ++
Cerrors.print_loc (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 ())
@@ -199,7 +199,7 @@ let valid_buffer_loc ib dloc loc =
let make_prompt () =
try
(Names.Id.to_string (Pfedit.get_current_proof_name ())) ^ " < "
- with _ ->
+ with Proof_global.NoCurrentProof ->
"Coq < "
(*let build_pending_list l =
@@ -331,7 +331,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:
@@ -345,8 +345,8 @@ let do_vernac () =
begin
try
ignore (raw_do_vernac top_buffer.tokens)
- with e ->
- ppnl (print_toplevel_error (process_error e))
+ with any ->
+ ppnl (print_toplevel_error (process_error any))
end;
flush_all()
@@ -365,6 +365,6 @@ let rec loop () =
| Errors.Drop -> ()
| End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0
| Errors.Quit -> exit 0
- | e ->
+ | any ->
msgerrnl (str"Anomaly. Please report.");
loop ()
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 33f6a0110..0f848ad4d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -52,7 +52,8 @@ let is_reset = function
let time = ref false
let display_cmd_header loc com =
- let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
+ let shorten s =
+ try (String.sub s 0 30)^"..." with Invalid_argument _ -> s in
let noblank s =
for i = 0 to String.length s - 1 do
match s.[i] with
@@ -204,7 +205,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 = Loc.unloc loc in
@@ -287,10 +288,10 @@ let rec vernac_com interpfun checknav (loc,com) =
let status = read_vernac_file verbosely (CUnix.make_suffix fname ".v") in
restore_translator_coqdoc st;
status
- with e ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
restore_translator_coqdoc st;
- raise e
+ raise reraise
end
| VernacList l ->
@@ -303,17 +304,16 @@ 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 -> ignore (interp v); raise HasNotFailed) v
- with e ->
+ with e when Errors.noncritical e ->
let e = Errors.push e in
match real_error e with
| HasNotFailed ->
errorlabstrm "Fail" (str "The command has not failed !")
| e ->
- (* Anomalies are re-raised by the next line *)
- let msg = Errors.print_no_anomaly e in
+ (* NB: e here cannot be an anomaly *)
if_verbose msg_info
(str "The command has indeed failed with message:" ++
- fnl () ++ str "=> " ++ hov 0 msg);
+ fnl () ++ str "=> " ++ hov 0 (Errors.print e));
true
end
@@ -338,10 +338,10 @@ let rec vernac_com interpfun checknav (loc,com) =
in
restore_timeout psh;
status
- with e ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
restore_timeout psh;
- raise e
+ raise reraise
in
try
checknav loc com;
@@ -350,7 +350,8 @@ let rec vernac_com interpfun checknav (loc,com) =
if !time then display_cmd_header loc com;
let com = if !time then VernacTime com else com in
interp com
- with e ->
+ with e -> (* TODO: restrict to Errors.noncritical or not ?
+ Morally, this is a reraise ... *)
let e = Errors.push e in
Format.set_formatter_out_channel stdout;
raise (DuringCommandInterp (loc, e))
@@ -386,6 +387,8 @@ and read_vernac_file verbosely s =
done;
assert false
with e -> (* whatever the exception *)
+ (* TODO: restrict to Errors.noncritical or not ?
+ Morally, this is a reraise ... *)
let e = Errors.push e in
Format.set_formatter_out_channel stdout;
close_input in_chan input; (* we must close the file first *)
@@ -432,6 +435,8 @@ let load_vernac verb file =
let _ = read_vernac_file verb file in
if !Flags.beautify_file then close_out !chan_beautify;
with e ->
+ (* TODO: restrict to Errors.noncritical or not ?
+ Morally, this is a reraise ... *)
let e = Errors.push e in
if !Flags.beautify_file then close_out !chan_beautify;
raise_with_file file e
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3eb33dce1..d3fea99ac 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -354,8 +354,7 @@ let dump_universes_gen g s =
Univ.dump_universes output_constraint g;
close ();
msg_info (str ("Universes written to file \""^s^"\"."))
- with
- e -> close (); raise e
+ with reraise -> close (); raise reraise
let dump_universes sorted s =
let g = Global.universes () in
@@ -378,21 +377,23 @@ let msg_found_library = function
msg_info (hov 0
(pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file))
-let msg_notfound_library loc qid = function
- | Library.LibUnmappedDir ->
- let dir = fst (repr_qualid qid) in
- user_err_loc (loc,"locate_library",
- strbrk "Cannot find a physical path bound to logical path " ++
- pr_dirpath dir ++ str".")
- | Library.LibNotFound ->
- msg_error (hov 0
- (strbrk "Unable to locate library " ++ pr_qualid qid ++ str"."))
- | e -> assert false
+let err_unmapped_library loc qid =
+ let dir = fst (repr_qualid qid) in
+ user_err_loc
+ (loc,"locate_library",
+ strbrk "Cannot find a physical path bound to logical path " ++
+ pr_dirpath dir ++ str".")
+
+let err_notfound_library loc qid =
+ msg_error
+ (hov 0 (strbrk "Unable to locate library " ++ pr_qualid qid ++ str"."))
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
+ | Library.LibUnmappedDir -> err_unmapped_library loc qid
+ | Library.LibNotFound -> err_notfound_library loc qid
let print_located_module r =
let (loc,qid) = qualid_of_reference r in
@@ -422,7 +423,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 *)
@@ -988,9 +989,11 @@ let vernac_declare_arguments local r l nargs flags =
| [[]] -> false | _ -> true in
let scopes = List.map (function
| None -> None
- | Some (o, k) ->
- try Some(ignore(Notation.find_scope k); k)
- with _ -> Some (Notation.find_delimiters_scope o k)) scopes in
+ | Some (o, k) ->
+ try ignore (Notation.find_scope k); Some k
+ with UserError _ ->
+ 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)
@@ -1496,7 +1499,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
@@ -1801,7 +1804,7 @@ let interp c =
if not (not mode && !Flags.program_mode && not isprogcmd) then
Flags.program_mode := mode;
true
- with e ->
+ with e when Errors.noncritical e ->
let e = Errors.push e in
match e with
| UnsafeSuccess ->
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index fdfa51427..9c5db8fd9 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -54,8 +54,8 @@ let call (opn,converted_args) =
hunk()
with
| Drop -> raise Drop
- | e ->
- let e = Errors.push e in
+ | reraise ->
+ let reraise = Errors.push reraise in
if !Flags.debug then
msg_debug (str"Vernac Interpreter " ++ str !loc);
- raise e
+ raise reraise
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 00:06:40 +0000