aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/tacextend.ml42
-rw-r--r--grammar/vernacextend.ml42
-rw-r--r--interp/constrextern.ml9
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/notation.ml6
-rw-r--r--kernel/csymtable.ml6
-rw-r--r--kernel/nativecode.ml4
-rw-r--r--kernel/nativelib.ml2
-rw-r--r--kernel/pre_env.ml2
-rw-r--r--kernel/safe_typing.ml3
-rw-r--r--lib/bigint.mli2
-rw-r--r--lib/errors.ml2
-rw-r--r--lib/flags.ml12
-rw-r--r--lib/pp.ml6
-rw-r--r--lib/profile.ml30
-rw-r--r--lib/serialize.ml6
-rw-r--r--lib/system.ml14
-rw-r--r--lib/xml_parser.ml4
-rw-r--r--library/declaremods.ml6
-rw-r--r--library/impargs.ml6
-rw-r--r--library/library.ml8
-rw-r--r--parsing/egramcoq.ml6
22 files changed, 73 insertions, 67 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index e3e957d95..23cf41bb2 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -168,7 +168,7 @@ 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
(Pp.app
(Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 9ae529ea0..b9b9dd8ea 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -55,7 +55,7 @@ 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
(Pp.app
(Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e2d40f23f..47753c158 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -228,10 +228,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 Failure _ -> mknot (loc,ntn,[]))
| [Terminal x], [] ->
(try mkprim (loc, Numeral (Bigint.of_string x))
- with _ -> mknot (loc,ntn,[]))
+ with Failure _ -> mknot (loc,ntn,[]))
| _ ->
mknot (loc,ntn,l)
@@ -810,12 +810,13 @@ 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 Failure _ -> [] 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 Failure _ -> [] in
subscopes,impls
| _ ->
[], [] in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1f76e3315..a677eb93e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -645,7 +645,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), [], [], []
diff --git a/interp/notation.ml b/interp/notation.ml
index e72151777..37ad387da 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -928,7 +928,7 @@ let _ =
let with_notation_protection f x =
let fs = freeze () in
try let a = f x in unfreeze fs; a
- with e ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
let () = unfreeze fs in
- raise e
+ raise reraise
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index bef5b751f..5dd4cb570 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -160,11 +160,11 @@ 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 ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
let () = print_string "can not compile \n" in
let () = Format.print_flush () in
- raise e
+ raise reraise
in
eval_to_patch env (to_memory ccfv)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index aeb5412e4..34f26086a 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -782,7 +782,7 @@ let subst s l =
else
let rec aux l =
match l with
- | MLlocal id -> (try LNmap.find id s with _ -> l)
+ | MLlocal id -> (try LNmap.find id s with Not_found -> l)
| MLglobal _ | MLprimitive _ | MLint _ -> l
| MLlam(params,body) -> MLlam(params, aux body)
| MLletrec(defs,body) ->
@@ -851,7 +851,7 @@ let commutative_cut annot a accu bs args =
let optimize gdef l =
let rec optimize s l =
match l with
- | MLlocal id -> (try LNmap.find id s with _ -> l)
+ | MLlocal id -> (try LNmap.find id s with Not_found -> l)
| MLglobal _ | MLprimitive _ | MLint _ -> l
| MLlam(params,body) ->
MLlam(params, optimize s body)
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 46125a2c7..6b2b4aa7c 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -91,7 +91,7 @@ let call_linker ~fatal prefix f upds =
with | Dynlink.Error e ->
let msg = "Dynlink error, " ^ Dynlink.error_message e in
if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg)
- | _ ->
+ | e when Errors.noncritical e ->
let msg = "Dynlink error" in
if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg));
match upds with Some upds -> update_locations upds | _ -> ()
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 2a467ad0a..f365d19c3 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 Failure _ -> raise Not_found
let env_of_rel n env =
{ env with
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fa565fa34..b2d08e977 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -881,7 +881,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/lib/bigint.mli b/lib/bigint.mli
index 754f10d67..8b61a1fb6 100644
--- a/lib/bigint.mli
+++ b/lib/bigint.mli
@@ -11,6 +11,8 @@
type bigint
val of_string : string -> bigint
+(** May a Failure just as [int_of_string] on non-numerical strings *)
+
val to_string : bigint -> string
val of_int : int -> bigint
diff --git a/lib/errors.ml b/lib/errors.ml
index 27baf4314..0d13fcd2f 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -73,7 +73,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
diff --git a/lib/flags.ml b/lib/flags.ml
index 4ad929052..bd31b4024 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -9,18 +9,18 @@
let with_option o f x =
let old = !o in o:=true;
try let r = f x in o := old; r
- with e ->
- let e = Backtrace.add_backtrace e in
+ with reraise ->
+ let reraise = Backtrace.add_backtrace reraise in
let () = o := old in
- raise e
+ 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 ->
- let e = Backtrace.add_backtrace e in
+ with reraise ->
+ let reraise = Backtrace.add_backtrace reraise in
let () = o := old in
- raise e
+ raise reraise
let boot = ref false
diff --git a/lib/pp.ml b/lib/pp.ml
index 99bd93411..85c623f0c 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -262,10 +262,10 @@ let pp_dirs ft =
fun (dirstream : _ ppdirs) ->
try
Stream.iter pp_dir dirstream; com_brk ft
- with e ->
- let e = Backtrace.add_backtrace e in
+ with reraise ->
+ let reraise = Backtrace.add_backtrace reraise in
let () = Format.pp_print_flush ft () in
- raise e
+ raise reraise
(* pretty print on stdout and stderr *)
diff --git a/lib/profile.ml b/lib/profile.ml
index b49a66e2f..6f878d2f6 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 Errors.noncritical e -> 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
let print_logical_stats a =
let (c, s, d) = CObj.obj_stats a in
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 218372afc..7c82d6b80 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -100,8 +100,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 *)
@@ -282,7 +282,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 Not_found | Failure _ -> None
in
let msg = raw_string l in
Fail (loc, msg)
diff --git a/lib/system.ml b/lib/system.ml
index 41201bd2d..a72958b99 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -105,12 +105,14 @@ let is_in_system_path filename =
is_in_path lpath filename
let open_trapping_failure name =
- try open_out_bin name with _ -> error ("Can't open " ^ name)
+ try open_out_bin name
+ with e when Errors.noncritical e -> error ("Can't open " ^ name)
let try_remove filename =
try Sys.remove filename
- with _ -> msg_warning
- (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
+ with e when Errors.noncritical e ->
+ msg_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 filename ch =
@@ -143,10 +145,10 @@ let extern_intern ?(warn=true) magic suffix =
try
marshal_out channel val_0;
close_out channel
- with e ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
let () = try_remove filename in
- raise e
+ raise reraise
with Sys_error s -> error ("System error: " ^ s)
and intern_state paths name =
try
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
index 108e22678..630992eb5 100644
--- a/lib/xml_parser.ml
+++ b/lib/xml_parser.ml
@@ -177,9 +177,9 @@ let do_parse xparser =
if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
Xml_lexer.close ();
x
- with e ->
+ with any ->
Xml_lexer.close ();
- raise (!xml_error (error_of_exn xparser e) xparser.source)
+ raise (!xml_error (error_of_exn xparser any) xparser.source)
let parse p = do_parse p
diff --git a/library/declaremods.ml b/library/declaremods.ml
index c30b2099f..366fb77a0 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -1004,11 +1004,11 @@ 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 *)
- let e = Errors.push e in
+ let reraise = Errors.push reraise in
let () = Summary.unfreeze_summaries fs in
- raise e
+ raise reraise
let declare_include interp_struct me_asts =
protect_summaries
diff --git a/library/impargs.ml b/library/impargs.ml
index 217169a61..56dca8e3f 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -75,10 +75,10 @@ let with_implicits flags f x =
let rslt = f x in
implicit_args := oflags;
rslt
- with e ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
let () = implicit_args := oflags in
- raise e
+ raise reraise
let set_maximality imps b =
(* Force maximal insertion on ending implicits (compatibility) *)
diff --git a/library/library.ml b/library/library.ml
index 0243968b9..a5f93c02c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -406,7 +406,7 @@ let fetch_opaque_table (f,pos,digest) =
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")
@@ -667,12 +667,12 @@ let save_library_to dir f =
| 0 -> ()
| _ -> anomaly (Pp.str "Library compilation failure")
end
- with e ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
let () = msg_warning (str ("Removed file "^f')) in
let () = close_out ch in
let () = Sys.remove f' in
- raise e
+ raise reraise
(************************************************************************)
(*s Display the memory use of a library. *)
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index e80d9301f..8edc56467 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -341,7 +341,7 @@ let _ =
let with_grammar_rule_protection f x =
let fs = freeze () in
try let a = f x in unfreeze fs; a
- with e ->
- let e = Errors.push e in
+ with reraise ->
+ let reraise = Errors.push reraise in
let () = unfreeze fs in
- raise e
+ raise reraise
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 00:55:54 +0000