aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml53
-rw-r--r--pretyping/cases.mli3
-rw-r--r--pretyping/coercion.ml10
-rw-r--r--pretyping/coercionops.ml2
-rw-r--r--pretyping/constr_matching.ml16
-rw-r--r--pretyping/evarconv.ml16
-rw-r--r--pretyping/evardefine.ml2
-rw-r--r--pretyping/glob_ops.ml4
-rw-r--r--pretyping/indrec.ml2
-rw-r--r--pretyping/keys.ml6
-rw-r--r--pretyping/patternops.ml6
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/tacred.ml8
-rw-r--r--pretyping/unification.ml10
14 files changed, 85 insertions, 55 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a459229256..4a29db0dcf 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -128,7 +128,8 @@ type 'a equation =
rhs : 'a rhs;
alias_stack : Name.t list;
eqn_loc : Loc.t option;
- used : bool ref }
+ used : int ref;
+ catch_all_vars : Id.t CAst.t list ref }
type 'a matrix = 'a equation list
@@ -514,7 +515,7 @@ let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with
let loc = pat.CAst.loc in
(* Check it is constructor of the right type *)
let ind' = inductive_of_constructor cstr in
- if eq_ind ind' ind then
+ if Ind.CanOrd.equal ind' ind then
(* Check the constructor has the right number of args *)
let ci = cstrs.(i-1) in
let nb_args_constr = ci.cs_nargs in
@@ -543,11 +544,34 @@ let check_all_variables env sigma typ mat =
error_bad_pattern ?loc env sigma cstr_sp typ)
mat
+let set_pattern_catch_all_var ?loc eqn = function
+ | Name id when not (Id.Set.mem id eqn.rhs.rhs_vars) ->
+ eqn.catch_all_vars := CAst.make ?loc id :: !(eqn.catch_all_vars)
+ | _ -> ()
+
+let warn_named_multi_catch_all =
+ CWarnings.create ~name:"unused-pattern-matching-variable" ~category:"pattern-matching"
+ (fun id ->
+ strbrk "Unused variable " ++ Id.print id ++ strbrk " catches more than one case.")
+
+let wildcard_id = Id.of_string "wildcard'"
+
+let is_wildcard id =
+ Id.equal (Id.of_string (Nameops.atompart_of_id id)) wildcard_id
+
let check_unused_pattern env eqn =
- if not !(eqn.used) then
- raise_pattern_matching_error ?loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns)
+ match !(eqn.used) with
+ | 0 -> raise_pattern_matching_error ?loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns)
+ | 1 -> ()
+ | _ ->
+ let warn {CAst.v = id; loc} =
+ (* Convention: Names starting with `_` and derivatives of Program's
+ "wildcard'" internal name deactivate the warning *)
+ if (Id.to_string id).[0] <> '_' && not (is_wildcard id)
+ then warn_named_multi_catch_all ?loc id in
+ List.iter warn !(eqn.catch_all_vars)
-let set_used_pattern eqn = eqn.used := true
+let set_used_pattern eqn = eqn.used := !(eqn.used) + 1
let extract_rhs pb =
match pb.mat with
@@ -1017,7 +1041,8 @@ let add_assert_false_case pb tomatch =
it = None };
alias_stack = Anonymous::aliasnames;
eqn_loc = None;
- used = ref false } ]
+ used = ref 0;
+ catch_all_vars = ref [] } ]
let adjust_impossible_cases sigma pb pred tomatch submat =
match submat with
@@ -1235,6 +1260,7 @@ let group_equations pb ind current cstrs mat =
let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in
brs.(i-1) <- (args, name, rest) :: brs.(i-1)
done;
+ set_pattern_catch_all_var ?loc:pat.CAst.loc eqn name;
if !only_default == None then only_default := Some true
| PatCstr (((_,i)),args,name) ->
(* This is a regular clause *)
@@ -1602,7 +1628,8 @@ let matx_of_eqns env eqns =
{ patterns = initial_lpat;
alias_stack = [];
eqn_loc = loc;
- used = ref false;
+ used = ref 0;
+ catch_all_vars = ref [];
rhs = rhs }
in List.map build_eqn eqns
@@ -1859,7 +1886,8 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
{ patterns = patl;
alias_stack = [];
eqn_loc = None;
- used = ref false;
+ used = ref 0;
+ catch_all_vars = ref [];
rhs = { rhs_env = pb_env;
(* we assume all vars are used; in practice we discard dependent
vars so that the field rhs_vars is normally not used *)
@@ -1879,7 +1907,8 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
[ { patterns = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl;
alias_stack = [];
eqn_loc = None;
- used = ref false;
+ used = ref 0;
+ catch_all_vars = ref [];
rhs = { rhs_env = pb_env;
rhs_vars = Id.Set.empty;
avoid_ids = avoid0;
@@ -1936,7 +1965,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
let realnal =
match t with
| Some {CAst.loc;v=(ind',realnal)} ->
- if not (eq_ind ind ind') then
+ if not (Ind.CanOrd.equal ind ind') then
user_err ?loc (str "Wrong inductive type.");
if not (Int.equal nrealargs_ctxt (List.length realnal)) then
anomaly (Pp.str "Ill-formed 'in' clause in cases.");
@@ -2149,7 +2178,7 @@ let constr_of_pat env sigma arsign pat avoid =
let name, avoid = match name with
Name n -> name, avoid
| Anonymous ->
- let previd, id = prime avoid (Name (Id.of_string "wildcard")) in
+ let id = next_ident_away wildcard_id avoid in
Name id, Id.Set.add id avoid
in
let r = Sorts.Relevant in (* TODO relevance *)
@@ -2164,7 +2193,7 @@ let constr_of_pat env sigma arsign pat avoid =
in
let (ind,u), params = dest_ind_family indf in
let params = List.map EConstr.of_constr params in
- if not (eq_ind ind cind) then error_bad_constructor ?loc env cstr ind;
+ if not (Ind.CanOrd.equal ind cind) then error_bad_constructor ?loc env cstr ind;
let cstrs = get_constructors env indf in
let ci = cstrs.(i-1) in
let nb_args_constr = ci.cs_nargs in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 8b1ec3aba0..9a986bc14c 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -68,7 +68,8 @@ type 'a equation =
rhs : 'a rhs;
alias_stack : Name.t list;
eqn_loc : Loc.t option;
- used : bool ref }
+ used : int ref;
+ catch_all_vars : Id.t CAst.t list ref }
type 'a matrix = 'a equation list
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index d759f82d35..6e6189796e 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -119,7 +119,7 @@ let disc_subset sigma x =
Ind (i,_) ->
let len = Array.length l in
let sigty = delayed_force sig_typ in
- if Int.equal len 2 && eq_ind i (Globnames.destIndRef sigty)
+ if Int.equal len 2 && Ind.CanOrd.equal i (Globnames.destIndRef sigty)
then
let (a, b) = pair_of_array l in
Some (a, b)
@@ -240,10 +240,10 @@ let coerce ?loc env sigma (x : EConstr.constr) (y : EConstr.constr)
let sigT = delayed_force sigT_typ in
let prod = delayed_force prod_typ in
(* Sigma types *)
- if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i'
- && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod))
+ if Int.equal len (Array.length l') && Int.equal len 2 && Ind.CanOrd.equal i i'
+ && (Ind.CanOrd.equal i (destIndRef sigT) || Ind.CanOrd.equal i (destIndRef prod))
then
- if eq_ind i (destIndRef sigT)
+ if Ind.CanOrd.equal i (destIndRef sigT)
then
begin
let (a, pb), (a', pb') =
@@ -303,7 +303,7 @@ let coerce ?loc env sigma (x : EConstr.constr) (y : EConstr.constr)
papp sigma prod_intro [| a'; b'; x ; y |])
end
else
- if eq_ind i i' && Int.equal len (Array.length l') then
+ if Ind.CanOrd.equal i i' && Int.equal len (Array.length l') then
(try subco sigma
with NoSubtacCoercion ->
let sigma, typ = Typing.type_of env sigma c in
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index 0c3eaa1da9..8ddc576d83 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -57,7 +57,7 @@ let cl_typ_ord t1 t2 = match t1, t2 with
| CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
| CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
| CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
- | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
+ | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
| _ -> pervasives_compare t1 t2 (** OK *)
module ClTyp = struct
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 419eeaa92a..a3f1c0b004 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -244,9 +244,9 @@ let matches_core env sigma allow_bound_rels
let open GlobRef in
match ref, EConstr.kind sigma c with
| VarRef id, Var id' -> Names.Id.equal id id'
- | ConstRef c, Const (c',_) -> Constant.equal c c'
- | IndRef i, Ind (i', _) -> Names.eq_ind i i'
- | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
+ | ConstRef c, Const (c',_) -> Environ.QConstant.equal env c c'
+ | IndRef i, Ind (i', _) -> Names.Ind.CanOrd.equal i i'
+ | ConstructRef c, Construct (c',u) -> Names.Construct.CanOrd.equal c c'
| _, _ -> false
in
let rec sorec ctx env subst p t =
@@ -307,11 +307,11 @@ let matches_core env sigma allow_bound_rels
| PApp (c1,arg1), App (c2,arg2) ->
(match c1, EConstr.kind sigma c2 with
- | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr))
+ | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Environ.QConstant.equal env r (Projection.constant pr))
|| Projection.unfolded pr ->
raise PatternMatchingFailure
| PProj (pr1,c1), Proj (pr,c) ->
- if Projection.equal pr1 pr then
+ if Environ.QProjection.equal env pr1 pr then
try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c) arg1 arg2
with Invalid_argument _ -> raise PatternMatchingFailure
else raise PatternMatchingFailure
@@ -324,7 +324,7 @@ let matches_core env sigma allow_bound_rels
with Invalid_argument _ -> raise PatternMatchingFailure)
| PApp (PRef (GlobRef.ConstRef c1), _), Proj (pr, c2)
- when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) ->
+ when Projection.unfolded pr || not (Environ.QConstant.equal env c1 (Projection.constant pr)) ->
raise PatternMatchingFailure
| PApp (c, args), Proj (pr, c2) ->
@@ -332,7 +332,7 @@ let matches_core env sigma allow_bound_rels
sorec ctx env subst p term
with Retyping.RetypeError _ -> raise PatternMatchingFailure)
- | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 ->
+ | PProj (p1,c1), Proj (p2,c2) when Environ.QProjection.equal env p1 p2 ->
sorec ctx env subst c1 c2
| PProd (na1,c1,d1), Prod(na2,c2,d2) ->
@@ -374,7 +374,7 @@ let matches_core env sigma allow_bound_rels
| Some ind1 ->
(* ppedrot: Something spooky going here. The comparison used to be
the generic one, so I may have broken something. *)
- if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure
+ if not (Ind.CanOrd.equal ind1 ci2.ci_ind) then raise PatternMatchingFailure
in
let () =
if not ci1.cip_extensible && not (Int.equal (List.length br1) n2)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a5311e162d..90af143a2d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -387,7 +387,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
| UnifFailure _ as x -> fail x)
| UnifFailure _ as x -> fail x)
| Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 ->
- if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
+ if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2)
then ise_stack2 true i q1 q2
else fail (UnifFailure (i, NotSameHead))
| Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1,
@@ -429,7 +429,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
(fun i -> ise_stack2 i a1 a2)]
else UnifFailure (i,NotSameHead)
| Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 ->
- if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
+ if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2)
then ise_stack2 i q1 q2
else (UnifFailure (i, NotSameHead))
| Stack.App _ :: _, Stack.App _ :: _ ->
@@ -566,11 +566,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
in
let compare_heads evd =
match EConstr.kind evd term, EConstr.kind evd term' with
- | Const (c, u), Const (c', u') when Constant.equal c c' ->
+ | Const (c, u), Const (c', u') when QConstant.equal env c c' ->
let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
check_strict evd u u'
| Const _, Const _ -> UnifFailure (evd, NotSameHead)
- | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.eq_ind ind ind' ->
+ | Ind ((mi,i) as ind , u), Ind (ind', u') when Names.Ind.CanOrd.equal ind ind' ->
if EInstance.is_empty u && EInstance.is_empty u' then Success evd
else
let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
@@ -589,7 +589,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
end
| Ind _, Ind _ -> UnifFailure (evd, NotSameHead)
| Construct (((mi,ind),ctor as cons), u), Construct (cons', u')
- when Names.eq_constructor cons cons' ->
+ when Names.Construct.CanOrd.equal cons cons' ->
if EInstance.is_empty u && EInstance.is_empty u' then Success evd
else
let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
@@ -831,7 +831,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
in
ise_try evd [f1; f2]
- | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' ->
+ | Proj (p, c), Proj (p', c') when QProjection.Repr.equal env (Projection.repr p) (Projection.repr p') ->
let f1 i =
ise_and i
[(fun i -> evar_conv_x flags env i CONV c c');
@@ -844,7 +844,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
ise_try evd [f1; f2]
(* Catch the p.c ~= p c' cases *)
- | Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' ->
+ | Proj (p,c), Const (p',u) when QConstant.equal env (Projection.constant p) p' ->
let res =
try Some (destApp evd (Retyping.expand_projection env evd p c []))
with Retyping.RetypeError _ -> None
@@ -855,7 +855,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
appr2
| None -> UnifFailure (evd,NotSameHead))
- | Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') ->
+ | Const (p,u), Proj (p',c') when QConstant.equal env p (Projection.constant p') ->
let res =
try Some (destApp evd (Retyping.expand_projection env evd p' c' []))
with Retyping.RetypeError _ -> None
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index eaf8c65811..13abf47413 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -206,7 +206,7 @@ let is_array_const env sigma c =
| Const (cst,_) ->
(match env.Environ.retroknowledge.Retroknowledge.retro_array with
| None -> false
- | Some cst' -> Constant.equal cst cst')
+ | Some cst' -> Environ.QConstant.equal env cst cst')
| _ -> false
let split_as_array env sigma0 = function
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index dc5fd80f9e..bdf3495479 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -91,7 +91,7 @@ let case_style_eq s1 s2 = let open Constr in match s1, s2 with
let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
| PatVar na1, PatVar na2 -> Name.equal na1 na2
| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
- eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+ Construct.CanOrd.equal c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
Name.equal na1 na2
| (PatVar _ | PatCstr _), _ -> false
@@ -109,7 +109,7 @@ let matching_var_kind_eq k1 k2 = match k1, k2 with
let tomatch_tuple_eq f (c1, p1) (c2, p2) =
let eqp {CAst.v=(i1, na1)} {CAst.v=(i2, na2)} =
- eq_ind i1 i2 && List.equal Name.equal na1 na2
+ Ind.CanOrd.equal i1 i2 && List.equal Name.equal na1 na2
in
let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in
f c1 c2 && eq_pred p1 p2
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 5be8f9f83c..5ffd919312 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -584,7 +584,7 @@ let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function
(List.map
(function ((mind',u'),dep',s') ->
let (sp',_) = mind' in
- if MutInd.equal sp sp' then
+ if QMutInd.equal env sp sp' then
let (mibi',mipi') = lookup_mind_specif env mind' in
((mind',u'),mibi',mipi',dep',s')
else
diff --git a/pretyping/keys.ml b/pretyping/keys.ml
index 7a7099c195..dd3488c1df 100644
--- a/pretyping/keys.ml
+++ b/pretyping/keys.ml
@@ -34,7 +34,7 @@ module KeyOrdered = struct
let hash gr =
match gr with
- | KGlob gr -> 9 + GlobRef.Ordered.hash gr
+ | KGlob gr -> 9 + GlobRef.CanOrd.hash gr
| KLam -> 0
| KLet -> 1
| KProd -> 2
@@ -49,14 +49,14 @@ module KeyOrdered = struct
let compare gr1 gr2 =
match gr1, gr2 with
- | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2
+ | KGlob gr1, KGlob gr2 -> GlobRef.CanOrd.compare gr1 gr2
| _, KGlob _ -> -1
| KGlob _, _ -> 1
| k, k' -> Int.compare (hash k) (hash k')
let equal k1 k2 =
match k1, k2 with
- | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2
+ | KGlob gr1, KGlob gr2 -> GlobRef.CanOrd.equal gr1 gr2
| _, KGlob _ -> false
| KGlob _, _ -> false
| k, k' -> k == k'
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 8c3d624f0f..b259945d9e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -23,7 +23,7 @@ open Environ
let case_info_pattern_eq i1 i2 =
i1.cip_style == i2.cip_style &&
- Option.equal eq_ind i1.cip_ind i2.cip_ind &&
+ Option.equal Ind.CanOrd.equal i1.cip_ind i2.cip_ind &&
Option.equal (List.equal (==)) i1.cip_ind_tags i2.cip_ind_tags &&
i1.cip_extensible == i2.cip_extensible
@@ -59,7 +59,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
| PCoFix (i1,f1), PCoFix (i2,f2) ->
Int.equal i1 i2 && rec_declaration_eq f1 f2
| PProj (p1, t1), PProj (p2, t2) ->
- Projection.equal p1 p2 && constr_pattern_eq t1 t2
+ Projection.CanOrd.equal p1 p2 && constr_pattern_eq t1 t2
| PInt i1, PInt i2 ->
Uint63.equal i1 i2
| PFloat f1, PFloat f2 ->
@@ -547,7 +547,7 @@ and pats_of_glob_branches loc metas vars ind brs =
true, [] (* ends with _ => _ *)
| PatCstr((indsp,j),lv,_), _, _ ->
let () = match ind with
- | Some sp when eq_ind sp indsp -> ()
+ | Some sp when Ind.CanOrd.equal sp indsp -> ()
| _ ->
err ?loc (Pp.str "All constructors must be in the same inductive type.")
in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 268ad2ae56..06f7d92e62 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -813,7 +813,7 @@ struct
try
let IndType (indf, args) = find_rectype !!env sigma ty in
let ((ind',u'),pars) = dest_ind_family indf in
- if eq_ind ind ind' then List.map EConstr.of_constr pars
+ if Ind.CanOrd.equal ind ind' then List.map EConstr.of_constr pars
else (* Let the usual code throw an error *) []
with Not_found -> []
else []
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9d15e98373..9cf7119709 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -82,7 +82,7 @@ type evaluable_reference =
| EvalEvar of EConstr.existential
let evaluable_reference_eq sigma r1 r2 = match r1, r2 with
-| EvalConst c1, EvalConst c2 -> Constant.equal c1 c2
+| EvalConst c1, EvalConst c2 -> Constant.CanOrd.equal c1 c2
| EvalVar id1, EvalVar id2 -> Id.equal id1 id2
| EvalRel i1, EvalRel i2 -> Int.equal i1 i2
| EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
@@ -995,7 +995,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
| CoFix _ | Fix _ -> s'
| Proj (p,t) when
(match EConstr.kind sigma constr with
- | Const (c', _) -> Constant.equal (Projection.constant p) c'
+ | Const (c', _) -> Constant.CanOrd.equal (Projection.constant p) c'
| _ -> false) ->
let npars = Projection.npars p in
if List.length stack <= npars then
@@ -1101,7 +1101,7 @@ let contextually byhead occs f env sigma t =
let match_constr_evaluable_ref sigma c evref =
match EConstr.kind sigma c, evref with
- | Const (c,u), EvalConstRef c' when Constant.equal c c' -> Some u
+ | Const (c,u), EvalConstRef c' when Constant.CanOrd.equal c c' -> Some u
| Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty
| _, _ -> None
@@ -1324,7 +1324,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
if isIndRef ref then
let ((mind,u),t) = reduce_to_ind_gen allow_product env sigma t in
begin match ref with
- | GlobRef.IndRef mind' when eq_ind mind mind' -> t
+ | GlobRef.IndRef mind' when Ind.CanOrd.equal mind mind' -> t
| _ -> error_cannot_recognize ref
end
else
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ccfb508964..4d37c0ef60 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -547,10 +547,10 @@ let oracle_order env cf1 cf2 =
| Some k2 ->
match k1, k2 with
| IsProj (p, _), IsKey (ConstKey (p',_))
- when Constant.equal (Projection.constant p) p' ->
+ when Environ.QConstant.equal env (Projection.constant p) p' ->
Some (not (Projection.unfolded p))
| IsKey (ConstKey (p,_)), IsProj (p', _)
- when Constant.equal p (Projection.constant p') ->
+ when Environ.QConstant.equal env p (Projection.constant p') ->
Some (Projection.unfolded p')
| _ ->
Some (Conv_oracle.oracle_order (fun x -> x)
@@ -796,7 +796,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c)
(* Fast path for projections. *)
- | Proj (p1,c1), Proj (p2,c2) when Constant.equal
+ | Proj (p1,c1), Proj (p2,c2) when Environ.QConstant.equal env
(Projection.constant p1) (Projection.constant p2) ->
(try unify_same_proj curenvnb cv_pb {opt with at_top = true}
substn c1 c2
@@ -844,7 +844,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
| Case (ci1,p1,_,c1,cl1), Case (ci2,p2,_,c2,cl2) ->
(try
- if not (eq_ind ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN);
+ if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then error_cannot_unify curenv sigma (cM,cN);
let opt' = {opt with at_top = true; with_types = false} in
Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true})
(unirec_rec curenvnb CONV opt'
@@ -914,7 +914,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
match EConstr.kind sigma c' with
| Meta _ -> true
| Evar _ -> true
- | Const (c, u) -> Constant.equal c (Projection.constant p)
+ | Const (c, u) -> Environ.QConstant.equal env c (Projection.constant p)
| _ -> false
in
let expand_proj c c' l =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 19:26:10 +0000