aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/refl_btauto.ml2
-rw-r--r--plugins/cc/ccalgo.ml9
-rw-r--r--plugins/extraction/extract_env.ml8
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--plugins/extraction/haskell.ml4
-rw-r--r--plugins/extraction/ocaml.ml4
-rw-r--r--plugins/firstorder/g_ground.ml42
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/fourier/fourierR.ml117
-rw-r--r--plugins/funind/functional_principles_proofs.ml22
-rw-r--r--plugins/funind/functional_principles_types.ml8
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/funind/glob_term_to_relation.ml13
-rw-r--r--plugins/funind/glob_termops.ml8
-rw-r--r--plugins/funind/indfun.ml12
-rw-r--r--plugins/funind/indfun_common.ml6
16 files changed, 117 insertions, 106 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index caa6eac2e..0b381407f 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -210,7 +210,7 @@ module Btauto = struct
let assign = List.map map_msg assign in
let l = str "[" ++ (concat (str ";" ++ spc ()) assign) ++ str "]" in
str "Not a tautology:" ++ spc () ++ l
- with _ -> (str "Not a tautology")
+ with e when Errors.noncritical e -> (str "Not a tautology")
in
Tacticals.tclFAIL 0 msg gl
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index c8238804a..473199cb2 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -400,9 +400,12 @@ let rec canonize_name c =
(* rebuild a term from a pattern and a substitution *)
let build_subst uf subst =
- Array.map (fun i ->
- try term uf i
- with _ -> anomaly (Pp.str "incomplete matching")) subst
+ Array.map
+ (fun i ->
+ try term uf i
+ with e when Errors.noncritical e ->
+ anomaly (Pp.str "incomplete matching"))
+ subst
let rec inst_pattern subst = function
PVar i ->
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 358fe2d01..a64cc3d70 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -489,8 +489,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
pp_with ft (d.preamble mo comment opened unsafe_needs);
pp_with ft (d.pp_struct struc);
Option.iter close_out cout;
- with e ->
- Option.iter close_out cout; raise e
+ with reraise ->
+ Option.iter close_out cout; raise reraise
end;
if not dry then Option.iter info_file fn;
(* Now, let's print the signature *)
@@ -503,8 +503,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
pp_with ft (d.pp_sig (signature_of_structure struc));
close_out cout;
- with e ->
- close_out cout; raise e
+ with reraise ->
+ close_out cout; raise reraise
end;
info_file si)
(if dry then None else si);
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 3ec9038c6..903a647fc 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -682,7 +682,7 @@ and extract_cst_app env mle mlt kn args =
let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
else mla
- with _ -> mla
+ with e when Errors.noncritical e -> mla
in
(* For strict languages, purely logical signatures with at least
one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 3925a2a2f..59dd5596e 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -86,7 +86,9 @@ let pp_global k r =
let rec pp_type par vl t =
let rec pp_rec par = function
| Tmeta _ | Tvar' _ -> assert false
- | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
+ | Tvar i ->
+ (try pr_id (List.nth vl (pred i))
+ with Failure _ -> (str "a" ++ int i))
| Tglob (r,[]) -> pp_global Type r
| Tglob (IndRef(kn,0),l)
when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 6c3054e2c..f3d6bcb98 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -127,7 +127,7 @@ let pp_type par vl t =
let rec pp_rec par = function
| Tmeta _ | Tvar' _ | Taxiom -> assert false
| Tvar i -> (try pp_tvar (List.nth vl (pred i))
- with _ -> (str "'a" ++ int i))
+ with Failure _ -> (str "'a" ++ int i))
| Tglob (r,[a1;a2]) when is_infix r ->
pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
| Tglob (r,[]) -> pp_global Type r
@@ -196,7 +196,7 @@ let rec pp_expr par env args =
let args = List.skipn (projection_arity r) args in
let record = List.hd args in
pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
- with _ -> apply (pp_global Term r))
+ with e when Errors.noncritical e -> apply (pp_global Term r))
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 94fce0e47..0cb45f51d 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -81,7 +81,7 @@ let gen_ground_tac flag taco ids bases gl=
extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
let result=ground_tac solver startseq gl in
qflag:=backup;result
- with e ->qflag:=backup;raise e
+ with reraise -> qflag:=backup;raise reraise
(* special for compatibility with Intuition
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index d39c6167b..baf1972e6 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -128,7 +128,7 @@ let mk_open_instance id gl m t=
| _-> anomaly (Pp.str "can't happen") in
let ntt=try
Pretyping.understand evmap env (raux m rawt)
- with _ ->
+ with e when Errors.noncritical e ->
error "Untypable instance, maybe higher-order non-prenex quantification" in
decompose_lam_n_assum m ntt
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 0ec82425d..a8c79c31e 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -44,8 +44,7 @@ let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;;
let flin_add f x c =
let cx = flin_coef f x in
- Constrhash.remove f.fhom x;
- Constrhash.add f.fhom x (rplus cx c);
+ Constrhash.replace f.fhom x (rplus cx c);
f
;;
let flin_add_cste f c =
@@ -92,6 +91,8 @@ let rec string_of_R_constr c =
|Const c -> string_of_R_constant c
| _ -> "not_of_constant"
+exception NoRational
+
let rec rational_of_constr c =
match kind_of_term c with
| Cast (c,_,_) -> (rational_of_constr c)
@@ -113,15 +114,17 @@ let rec rational_of_constr c =
| "Rminus" ->
rminus (rational_of_constr args.(0))
(rational_of_constr args.(1))
- | _ -> failwith "not a rational")
+ | _ -> raise NoRational)
| Const kn ->
(match (string_of_R_constant kn) with
"R1" -> r1
|"R0" -> r0
- | _ -> failwith "not a rational")
- | _ -> failwith "not a rational"
+ | _ -> raise NoRational)
+ | _ -> raise NoRational
;;
+exception NoLinear
+
let rec flin_of_constr c =
try(
match kind_of_term c with
@@ -137,35 +140,34 @@ let rec flin_of_constr c =
flin_minus (flin_of_constr args.(0))
(flin_of_constr args.(1))
| "Rmult"->
- (try (let a=(rational_of_constr args.(0)) in
- try (let b = (rational_of_constr args.(1)) in
- (flin_add_cste (flin_zero()) (rmult a b)))
- with _-> (flin_add (flin_zero())
- args.(1)
- a))
- with _-> (flin_add (flin_zero())
- args.(0)
- (rational_of_constr args.(1))))
+ (try
+ let a = rational_of_constr args.(0) in
+ try
+ let b = rational_of_constr args.(1) in
+ flin_add_cste (flin_zero()) (rmult a b)
+ with NoRational ->
+ flin_add (flin_zero()) args.(1) a
+ with NoRational ->
+ flin_add (flin_zero()) args.(0)
+ (rational_of_constr args.(1)))
| "Rinv"->
- let a=(rational_of_constr args.(0)) in
- flin_add_cste (flin_zero()) (rinv a)
+ let a = rational_of_constr args.(0) in
+ flin_add_cste (flin_zero()) (rinv a)
| "Rdiv"->
- (let b=(rational_of_constr args.(1)) in
- try (let a = (rational_of_constr args.(0)) in
- (flin_add_cste (flin_zero()) (rdiv a b)))
- with _-> (flin_add (flin_zero())
- args.(0)
- (rinv b)))
- |_->assert false)
+ (let b = rational_of_constr args.(1) in
+ try
+ let a = rational_of_constr args.(0) in
+ flin_add_cste (flin_zero()) (rdiv a b)
+ with NoRational ->
+ flin_add (flin_zero()) args.(0) (rinv b))
+ |_-> raise NoLinear)
| Const c ->
(match (string_of_R_constant c) with
"R1" -> flin_one ()
|"R0" -> flin_zero ()
- |_-> assert false)
- |_-> assert false)
- with _ -> flin_add (flin_zero())
- c
- r1
+ |_-> raise NoLinear)
+ |_-> raise NoLinear)
+ with NoRational | NoLinear -> flin_add (flin_zero()) c r1
;;
let flin_to_alist f =
@@ -186,52 +188,55 @@ type hineq={hname:constr; (* le nom de l'hypothèse *)
(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
*)
+
+exception NoIneq
+
let ineq1_of_constr (h,t) =
match (kind_of_term t) with
- App (f,args) ->
- (match kind_of_term f with
- Const c when Array.length args = 2 ->
- let t1= args.(0) in
- let t2= args.(1) in
+ | App (f,args) ->
+ (match kind_of_term f with
+ | Const c when Array.length args = 2 ->
+ let t1= args.(0) in
+ let t2= args.(1) in
(match (string_of_R_constant c) with
- "Rlt" -> [{hname=h;
+ |"Rlt" -> [{hname=h;
htype="Rlt";
hleft=t1;
hright=t2;
hflin= flin_minus (flin_of_constr t1)
(flin_of_constr t2);
hstrict=true}]
- |"Rgt" -> [{hname=h;
+ |"Rgt" -> [{hname=h;
htype="Rgt";
hleft=t2;
hright=t1;
hflin= flin_minus (flin_of_constr t2)
(flin_of_constr t1);
hstrict=true}]
- |"Rle" -> [{hname=h;
+ |"Rle" -> [{hname=h;
htype="Rle";
hleft=t1;
hright=t2;
hflin= flin_minus (flin_of_constr t1)
(flin_of_constr t2);
hstrict=false}]
- |"Rge" -> [{hname=h;
+ |"Rge" -> [{hname=h;
htype="Rge";
hleft=t2;
hright=t1;
hflin= flin_minus (flin_of_constr t2)
(flin_of_constr t1);
hstrict=false}]
- |_->assert false)
+ |_-> raise NoIneq)
| Ind (kn,i) ->
- if IndRef(kn,i) = Coqlib.glob_eq then
- let t0= args.(0) in
- let t1= args.(1) in
- let t2= args.(2) in
- (match (kind_of_term t0) with
- Const c ->
- (match (string_of_R_constant c) with
- "R"->
+ if not (eq_gr (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq;
+ let t0= args.(0) in
+ let t1= args.(1) in
+ let t2= args.(2) in
+ (match (kind_of_term t0) with
+ | Const c ->
+ (match (string_of_R_constant c) with
+ | "R"->
[{hname=h;
htype="eqTLR";
hleft=t1;
@@ -246,12 +251,10 @@ let ineq1_of_constr (h,t) =
hflin= flin_minus (flin_of_constr t2)
(flin_of_constr t1);
hstrict=false}]
- |_-> assert false)
- |_-> assert false)
- else
- assert false
- |_-> assert false)
- |_-> assert false
+ |_-> raise NoIneq)
+ |_-> raise NoIneq)
+ |_-> raise NoIneq)
+ |_-> raise NoIneq
;;
(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
@@ -459,6 +462,8 @@ let mkAppL a =
mkApp(List.hd l, Array.of_list (List.tl l))
;;
+exception GoalDone
+
(* Résolution d'inéquations linéaires dans R *)
let rec fourier gl=
Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
@@ -490,16 +495,16 @@ let rec fourier gl=
(tclTHEN (apply (get coq_Rfourier_not_lt_ge))
(intro_using fhyp))
fourier)
- |_->assert false)
- |_->assert false
+ |_-> raise GoalDone)
+ |_-> raise GoalDone
in tac gl)
- with _ ->
+ with GoalDone ->
(* les hypothèses *)
let hyps = List.map (fun (h,t)-> (mkVar h,t))
(list_of_sign (pf_hyps gl)) in
let lineq =ref [] in
List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
- with _ -> ())
+ with NoIneq _ -> ())
hyps;
(* lineq = les inéquations découlant des hypothèses *)
if !lineq=[] then Errors.error "No inequalities";
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f8ea1d528..fdbd6cabd 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -72,16 +72,16 @@ let do_observe_tac s tac g =
let v = tac g in
ignore(Stack.pop debug_queue);
v
- with e ->
- begin
+ with reraise ->
+ begin
if not (Stack.is_empty debug_queue)
then
- begin
- let e : exn = Cerrors.process_vernac_interp_error e in
- print_debug_queue true e
+ begin
+ let reraise : exn = Cerrors.process_vernac_interp_error reraise in
+ print_debug_queue true reraise
end
- ;
- raise e
+ ;
+ raise reraise
end
let observe_tac_stream s tac g =
@@ -145,7 +145,7 @@ let is_trivial_eq t =
eq_constr t1 t2 && eq_constr a1 a2
| _ -> false
end
- with _ -> false
+ with e when Errors.noncritical e -> false
in
(* observe (str "is_trivial_eq " ++ Printer.pr_lconstr t ++ (if res then str " true" else str " false")); *)
res
@@ -171,7 +171,7 @@ let is_incompatible_eq t =
(eq_constr u1 u2 &&
incompatible_constructor_terms t1 t2)
| _ -> false
- with _ -> false
+ with e when Errors.noncritical e -> false
in
if res then observe (str "is_incompatible_eq " ++ Printer.pr_lconstr t);
res
@@ -258,7 +258,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type =
then
(jmeq_refl (),(args.(1),args.(0)),(args.(3),args.(2)),args.(0))
else nochange "not an equality"
- with _ -> nochange "not an equality"
+ with e when Errors.noncritical e -> nochange "not an equality"
in
if not ((closed0 (fst t1)) && (closed0 (snd t1)))then nochange "not a closed lhs";
let rec compute_substitution sub t1 t2 =
@@ -629,7 +629,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
let my_orelse tac1 tac2 g =
try
tac1 g
- with e ->
+ with e when Errors.noncritical e ->
(* observe (str "using snd tac since : " ++ Errors.print e); *)
tac2 g
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 7f05c3b0e..09637d273 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -363,7 +363,7 @@ let generate_functional_principle
Don't forget to close the goal if an error is raised !!!!
*)
save false new_princ_name entry g_kind hook
- with e ->
+ with e when Errors.noncritical e ->
begin
begin
try
@@ -375,7 +375,7 @@ let generate_functional_principle
then Pfedit.delete_current_proof ()
else ()
else ()
- with _ -> ()
+ with e when Errors.noncritical e -> ()
end;
raise (Defining_principle e)
end
@@ -516,7 +516,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
0
(prove_princ_for_struct false 0 (Array.of_list funs))
(fun _ _ _ -> ())
- with e ->
+ with e when Errors.noncritical e ->
begin
begin
try
@@ -528,7 +528,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
then Pfedit.delete_current_proof ()
else ()
else ()
- with _ -> ()
+ with e when Errors.noncritical e -> ()
end;
raise (Defining_principle e)
end
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index ef2276134..1ccfe3c31 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -209,14 +209,14 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
try Functional_principles_types.build_scheme fas
with Functional_principles_types.No_graph_found ->
Errors.error ("Cannot generate induction principle(s)")
- | e ->
+ | e when Errors.noncritical e ->
let names = List.map (fun (_,na,_) -> na) fas in
warning_error names e
end
| _ -> assert false (* we can only have non empty list *)
end
- | e ->
+ | e when Errors.noncritical e ->
let names = List.map (fun (_,na,_) -> na) fas in
warning_error names e
end
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 9ec935cfd..fe48cbd88 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -912,7 +912,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
try
observe (str "computing new type for eq : " ++ pr_glob_constr rt);
let t' =
- try Pretyping.understand Evd.empty env t with _ -> raise Continue
+ try Pretyping.understand Evd.empty env t
+ with e when Errors.noncritical e -> raise Continue
in
let is_in_b = is_free_in id b in
let _keep_eq =
@@ -1211,7 +1212,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool)
l := param::!l
)
rels_params.(0)
- with _ ->
+ with e when Errors.noncritical e ->
()
in
List.rev !l
@@ -1417,7 +1418,7 @@ let do_build_inductive
in
observe (msg);
raise e
- | e ->
+ | reraise ->
let _time3 = System.get_time () in
(* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
let repacked_rel_inds =
@@ -1428,16 +1429,16 @@ let do_build_inductive
str "while trying to define"++ spc () ++
Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
++ fnl () ++
- Errors.print e
+ Errors.print reraise
in
observe msg;
- raise e
+ raise reraise
let build_inductive funnames funsargs returned_types rtl =
try
do_build_inductive funnames funsargs returned_types rtl
- with e -> raise (Building_graph e)
+ with e when Errors.noncritical e -> raise (Building_graph e)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 0159a0aee..6b4fbeef4 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -531,8 +531,8 @@ let rec are_unifiable_aux = function
then raise NotUnifiable
else
let eqs' =
- try ((List.combine cpl1 cpl2)@eqs)
- with _ -> anomaly (Pp.str "are_unifiable_aux")
+ try (List.combine cpl1 cpl2) @ eqs
+ with Invalid_argument _ -> anomaly (Pp.str "are_unifiable_aux")
in
are_unifiable_aux eqs'
@@ -553,8 +553,8 @@ let rec eq_cases_pattern_aux = function
then raise NotUnifiable
else
let eqs' =
- try ((List.combine cpl1 cpl2)@eqs)
- with _ -> anomaly (Pp.str "eq_cases_pattern_aux")
+ try (List.combine cpl1 cpl2) @ eqs
+ with Invalid_argument _ -> anomaly (Pp.str "eq_cases_pattern_aux")
in
eq_cases_pattern_aux eqs'
| _ -> raise NotUnifiable
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d58a6f038..f0f76860a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -164,8 +164,8 @@ let build_newrecursive
sigma rec_sign rec_impls def
)
lnameargsardef
- with e ->
- States.unfreeze fs; raise e in
+ with reraise ->
+ States.unfreeze fs; raise reraise in
States.unfreeze fs; def
in
recdef,rec_impls
@@ -249,12 +249,12 @@ let derive_inversion fix_names =
(fun id -> destInd (Constrintern.global_reference (mk_rel_id id)))
fix_names
)
- with e ->
+ with e when Errors.noncritical e ->
let e' = Cerrors.process_vernac_interp_error e in
msg_warning
(str "Cannot build inversion information" ++
if do_observe () then (fnl() ++ Errors.print e') else mt ())
- with _ -> ()
+ with e when Errors.noncritical e -> ()
let warning_error names e =
let e = Cerrors.process_vernac_interp_error e in
@@ -351,7 +351,7 @@ let generate_principle on_error
Array.iter (add_Function is_general) funs_kn;
()
end
- with e ->
+ with e when Errors.noncritical e ->
on_error names e
let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
@@ -414,7 +414,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
);
derive_inversion [fname]
- with e ->
+ with e when Errors.noncritical e ->
(* No proof done *)
()
in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index d6a017d08..56660cd69 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -118,7 +118,7 @@ let def_of_const t =
(try (match Declareops.body_of_constant (Global.lookup_constant sp) with
| Some c -> Lazyconstr.force c
| _ -> assert false)
- with _ -> assert false)
+ with Not_found -> assert false)
|_ -> assert false
let coq_constant s =
@@ -204,13 +204,13 @@ let with_full_print f a =
Dumpglob.continue ();
res
with
- | e ->
+ | reraise ->
Impargs.make_implicit_args old_implicit_args;
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
Flags.raw_print := old_rawprint;
Dumpglob.continue ();
- raise e
+ raise reraise
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 19:40:57 +0000