aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/evarsolve.ml4
-rw-r--r--pretyping/nativenorm.ml10
-rw-r--r--pretyping/pretyping.ml22
-rw-r--r--pretyping/recordops.ml8
-rw-r--r--pretyping/typeclasses.ml10
-rw-r--r--pretyping/unification.ml13
9 files changed, 42 insertions, 31 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7516951e8..e16e8e1cc 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2257,7 +2257,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
(* The tycon may be ill-typed after abstraction. *)
let env' = push_rel_context (context_of_arsign sign) env in
ignore(Typing.sort_of env' !evdref pred); pred
- with _ ->
+ with e when Errors.noncritical e ->
let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
lift nar t
in Option.get tycon, pred
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index aa172fc2a..9c61d3f06 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -335,7 +335,7 @@ let apply_coercion env sigma p hj typ_cl =
jres),
jres.uj_type)
(hj,typ_cl) p)
- with _ -> anomaly (Pp.str "apply_coercion")
+ with e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
let inh_app_fun env evd j =
let t = whd_betadeltaiota env evd j.uj_type in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 7c63c970d..52c930e62 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -527,7 +527,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
in Success evd'
with Univ.UniverseInconsistency _ ->
UnifFailure (evd,UnifUnivInconsistency)
- | _ -> UnifFailure (evd,NotSameHead))
+ | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead))
| Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty ->
ise_and evd
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 01878024b..6818d84fe 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1042,7 +1042,7 @@ let check_evar_instance evd evk1 body conv_algo =
(* FIXME: The body might be ill-typed when this is called from w_merge *)
let ty =
try Retyping.get_type_of evenv evd body
- with _ -> error "Ill-typed evar instance"
+ with e when Errors.noncritical e -> error "Ill-typed evar instance"
in
match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with
| Success evd -> evd
@@ -1248,7 +1248,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
imitate envk t in
t::l
- with _ -> l in
+ with e when Errors.noncritical e -> l in
(match candidates with
| [x] -> x
| _ ->
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index a4f00bc45..887773311 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -43,7 +43,7 @@ let decompose_prod env t =
let app_type env c =
let t = whd_betadeltaiota env c in
- try destApp t with _ -> (t,[||])
+ try destApp t with DestKO -> (t,[||])
let find_rectype_a env c =
@@ -192,7 +192,7 @@ and nf_type_sort env v =
match kind_of_value v with
| Vaccu accu ->
let t,s = nf_accu_type env accu in
- let s = try destSort s with _ -> assert false in
+ let s = try destSort s with DestKO -> assert false in
t, s
| _ -> assert false
@@ -214,7 +214,7 @@ and nf_accu_type env accu =
and nf_args env accu t =
let aux arg (t,l) =
- let _,dom,codom = try decompose_prod env t with _ -> exit 123 in
+ let _,dom,codom = try decompose_prod env t with DestKO -> exit 123 in
let c = nf_val env arg dom in
(subst1 c codom, c::l)
in
@@ -226,7 +226,7 @@ and nf_bargs env b t =
let len = block_size b in
Array.init len
(fun i ->
- let _,dom,codom = try decompose_prod env !t with _ -> exit 124 in
+ let _,dom,codom = try decompose_prod env !t with DestKO -> exit 124 in
let c = nf_val env (block_field b i) dom in
t := subst1 c codom; c)
@@ -313,7 +313,7 @@ and nf_predicate env ind mip params v pT =
| Vfun f, Prod _ ->
let k = nb_rel env in
let vb = f (mk_rel_accu k) in
- let name,dom,codom = try decompose_prod env pT with _ -> exit 121 in
+ let name,dom,codom = try decompose_prod env pT with DestKO -> exit 121 in
let dep,body =
nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
dep, mkLambda(name,dom,body)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0321707b0..f7b929f0f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -68,8 +68,9 @@ let search_guard loc env possible_indexes fixdefs =
if List.for_all is_singleton possible_indexes then
let indexes = Array.of_list (List.map List.hd possible_indexes) in
let fix = ((indexes, 0),fixdefs) in
- (try check_fix env fix with
- | e -> let e = Errors.push e in Loc.raise loc e);
+ (try check_fix env fix
+ with e when Errors.noncritical e ->
+ let e = Errors.push e in Loc.raise loc e);
indexes
else
(* we now search recursively amoungst all combinations *)
@@ -112,9 +113,11 @@ let resolve_evars env evdref fail_evar resolve_classes =
~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref;
);
(* Resolve eagerly, potentially making wrong choices *)
- evdref := (try consider_remaining_unif_problems
- ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
- with e -> let e = Errors.push e in if fail_evar then raise e else !evdref)
+ evdref :=
+ (try consider_remaining_unif_problems
+ ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
+ with e when Errors.noncritical e ->
+ let e = Errors.push e in if fail_evar then raise e else !evdref)
let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
let evdref = ref evd in
@@ -362,9 +365,12 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
| GCoFix i ->
let cofix = (i,(names,ftys,fdefs)) in
- (try check_cofix env cofix with e -> let e = Errors.push e in Loc.raise loc e);
- make_judge (mkCoFix cofix) ftys.(i) in
- inh_conv_coerce_to_tycon loc env evdref fixj tycon
+ (try check_cofix env cofix
+ with e when Errors.noncritical e ->
+ let e = Errors.push e in Loc.raise loc e);
+ make_judge (mkCoFix cofix) ftys.(i)
+ in
+ inh_conv_coerce_to_tycon loc env evdref fixj tycon
| GSort (loc,s) ->
let j = pretype_sort evdref s in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index cc6ec1e95..7c2ac1a27 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -208,16 +208,16 @@ let cs_pattern_of_constr t =
match kind_of_term t with
App (f,vargs) ->
begin
- try Const_cs (global_of_constr f) , -1, Array.to_list vargs with
- _ -> raise Not_found
+ try Const_cs (global_of_constr f) , -1, Array.to_list vargs
+ with e when Errors.noncritical e -> raise Not_found
end
| Rel n -> Default_cs, pred n, []
| Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, -1, [a; Termops.pop b]
| Sort s -> Sort_cs (family_of_sort s), -1, []
| _ ->
begin
- try Const_cs (global_of_constr t) , -1, [] with
- _ -> raise Not_found
+ try Const_cs (global_of_constr t) , -1, []
+ with e when Errors.noncritical e -> raise Not_found
end
(* Intended to always succeed *)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c477013d8..80207f652 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -115,7 +115,7 @@ let _ =
let class_info c =
try Gmap.find c !classes
- with _ -> not_a_class (Global.env()) (constr_of_global c)
+ with Not_found -> not_a_class (Global.env()) (constr_of_global c)
let global_class_of_constr env c =
try class_info (global_of_constr c)
@@ -129,7 +129,9 @@ let dest_class_arity env c =
let rels, c = Term.decompose_prod_assum c in
rels, dest_class_app env c
-let class_of_constr c = try Some (dest_class_arity (Global.env ()) c) with _ -> None
+let class_of_constr c =
+ try Some (dest_class_arity (Global.env ()) c)
+ with e when Errors.noncritical e -> None
let rec is_class_type evd c =
match kind_of_term c with
@@ -216,7 +218,7 @@ let rebuild_class cl =
try
let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
set_typeclass_transparency cst false false; cl
- with _ -> cl
+ with e when Errors.noncritical e -> cl
let class_input : typeclass -> obj =
declare_object
@@ -239,7 +241,7 @@ let check_instance env sigma c =
let (evd, c) = resolve_one_typeclass env sigma
(Retyping.get_type_of env sigma c) in
Evd.is_empty (Evd.undefined_evars evd)
- with _ -> false
+ with e when Errors.noncritical e -> false
let build_subclasses ~check env sigma glob pri =
let _id = Nametab.basename_of_global glob in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e287ca52a..ec6eeea12 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -425,8 +425,9 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
then Evd.set_leq_sort sigma s1 s2
else Evd.set_eq_sort sigma s1 s2
in (sigma', metasubst, evarsubst)
- with _ -> error_cannot_unify curenv sigma (m,n))
-
+ with e when Errors.noncritical e ->
+ error_cannot_unify curenv sigma (m,n))
+
| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
unirec_rec (push (na,t1) curenvnb) CONV true wt
(unirec_rec curenvnb CONV true false substn t1 t2) c1 c2
@@ -708,10 +709,12 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
else (right, st2, res)
| (IsSuperType,IsSubType) ->
(try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1)
- with _ -> (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
+ with e when Errors.noncritical e ->
+ (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
| (IsSubType,IsSuperType) ->
(try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2)
- with _ -> (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
+ with e when Errors.noncritical e ->
+ (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
(* Unification
*
@@ -917,7 +920,7 @@ let w_merge env with_types flags (evd,metas,evars) =
let rec process_eqns failures = function
| (mv,status,c)::eqns ->
(match (try Inl (unify_type env evd flags mv status c)
- with e -> Inr e)
+ with e when Errors.noncritical e -> Inr e)
with
| Inr e -> process_eqns (((mv,status,c),e)::failures) eqns
| Inl (evd,metas,evars) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 02:47:26 +0000