summaryrefslogtreecommitdiff
path: root/plugins/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac')
-rw-r--r--plugins/subtac/g_subtac.ml43
-rw-r--r--plugins/subtac/subtac.ml4
-rw-r--r--plugins/subtac/subtac_cases.ml5
-rw-r--r--plugins/subtac/subtac_coercion.ml4
-rw-r--r--plugins/subtac/subtac_command.ml4
-rw-r--r--plugins/subtac/subtac_obligations.ml7
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml6
-rw-r--r--plugins/subtac/subtac_utils.ml8
8 files changed, 23 insertions, 18 deletions
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index 956ccf09..6e7a8d32 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -90,7 +90,8 @@ VERNAC COMMAND EXTEND Subtac
let try_catch_exn f e =
try f e
- with exn -> errorlabstrm "Program" (Errors.print exn)
+ with exn when Errors.noncritical exn ->
+ errorlabstrm "Program" (Errors.print exn)
let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e
let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 281e981b..ad248bfb 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -221,6 +221,6 @@ let subtac (loc, command) =
| (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
Loc.Exc_located (loc, e') as e) -> raise e
- | e ->
+ | reraise ->
(* msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
- raise e
+ raise reraise
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 221b57ee..0b1ed9bb 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -342,7 +342,7 @@ let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
let pred = predicate 0 c in
let env' = push_rel_context (context_of_arsign arsign) env in
ignore(Typing.sort_of env' evm pred); pred
- with _ -> lift nar c
+ with e when Errors.noncritical e -> lift nar c
module Cases_F(Coercion : Coercion.S) : S = struct
@@ -1465,7 +1465,8 @@ let extract_arity_signatures env0 tomatchl tmsign =
| None -> list_tabulate (fun _ -> Anonymous) nrealargs in
let arsign = fst (get_arity env0 indf) in
(na,None,build_dependent_inductive env0 indf)
- ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign with _ -> assert false) in
+ ::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign
+ with e when Errors.noncritical e -> assert false) in
let rec buildrec = function
| [],[] -> []
| (_,tm)::ltm, x::tmsign ->
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 168a799d..0c03fb4c 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -356,7 +356,7 @@ module Coercion = struct
jres),
jres.uj_type)
(hj,typ_cl) p)
- with _ -> anomaly "apply_coercion"
+ with e when Errors.noncritical e -> anomaly "apply_coercion"
let inh_app_fun env isevars j =
let isevars = ref isevars in
@@ -506,5 +506,5 @@ module Coercion = struct
with NoSubtacCoercion ->
error_cannot_coerce env' isevars (t, t'))
else isevars
- with _ -> isevars
+ with e when Errors.noncritical e -> isevars
end
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 14a09032..537a8301 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -248,7 +248,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
| [(_, None, t); (_, None, u)], Sort (Prop Null)
when Reductionops.is_conv env !isevars t u -> t
| _, _ -> error ()
- with _ -> error ()
+ with e when Errors.noncritical e -> error ()
in
let measure = interp_casted_constr isevars binders_env measure relargty in
let wf_rel, wf_rel_fun, measure_fn =
@@ -440,7 +440,7 @@ let interp_recursive fixkind l =
let sort = Retyping.get_type_of env !evdref t in
let fixprot =
try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|])
- with e -> t
+ with e when Errors.noncritical e -> t
in
(id,None,fixprot) :: env')
[] fixnames fixtypes
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index dfcc8526..d8f46098 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -121,7 +121,7 @@ let obl_substitution expand obls deps =
let xobl = obls.(x) in
let oblb =
try get_obligation_body expand xobl
- with _ -> assert(false)
+ with e when Errors.noncritical e -> assert(false)
in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
deps []
@@ -498,7 +498,8 @@ let rec solve_obligation prg num tac =
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
let res = try update_obls prg obls (pred rem)
- with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e))
+ with e when Errors.noncritical e ->
+ pperror (Errors.print (Cerrors.process_vernac_interp_error e))
in
match res with
| Remain n when n > 0 ->
@@ -552,7 +553,7 @@ and solve_obligation_by_tac prg obls i tac =
| Refiner.FailError (_, s) ->
user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
| Util.Anomaly _ as e -> raise e
- | e -> false
+ | e when Errors.noncritical e -> false
and solve_prg_obligations prg ?oblset tac =
let obls, rem = prg.prg_obligations in
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 95e756ab..f0579711 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -302,7 +302,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
| GCoFix i ->
let cofix = (i,(names,ftys,fdefs)) in
- (try check_cofix env cofix with e -> Loc.raise loc e);
+ (try check_cofix env cofix
+ with e when Errors.noncritical e -> Loc.raise loc e);
make_judge (mkCoFix cofix) ftys.(i) in
inh_conv_coerce_to_tycon loc env evdref fixj tycon
@@ -601,7 +602,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
~split:true ~fail:true env !evdref;
evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
~split:true ~fail:false env !evdref
- with e -> if fail_evar then raise e else ());
+ with e when Errors.noncritical e ->
+ if fail_evar then raise e else ());
evdref := consider_remaining_unif_problems env !evdref;
let c = if expand_evar then nf_evar !evdref c' else c' in
if fail_evar then check_evars env Evd.empty !evdref c;
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index fbb44811..e32bb9e0 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -232,7 +232,7 @@ let build_dependent_sum l =
let hyptype = substl names t in
trace (spc () ++ str ("treating evar " ^ string_of_id n));
(try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
- with _ -> ());
+ with e when Errors.noncritical e -> ());
let tac = assert_tac (Name n) hyptype in
let conttac =
(fun cont ->
@@ -331,7 +331,7 @@ let destruct_ex ext ex =
Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 ->
let (dom, rng) =
try (args.(0), args.(1))
- with _ -> assert(false)
+ with e when Errors.noncritical e -> assert(false)
in
let pi1 = (mk_ex_pi1 dom rng acc) in
let rng_body =
@@ -375,9 +375,9 @@ let solve_by_tac evi t =
Inductiveops.control_only_guard (Global.env ())
const.Entries.const_entry_body;
const.Entries.const_entry_body
- with e ->
+ with reraise ->
Pfedit.delete_current_proof();
- raise e
+ raise reraise
(* let apply_tac t goal = t goal *)
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-30 03:04:24 +0000