aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml6
-rw-r--r--pretyping/coercion.ml10
-rw-r--r--pretyping/coercionops.ml2
-rw-r--r--pretyping/constr_matching.ml4
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/glob_ops.ml2
-rw-r--r--pretyping/patternops.ml4
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/unification.ml2
10 files changed, 18 insertions, 18 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a459229256..d48951e84a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -514,7 +514,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
@@ -1936,7 +1936,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.");
@@ -2164,7 +2164,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/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 71ef166ff0..0200b32ef2 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -245,7 +245,7 @@ let matches_core env sigma allow_bound_rels
match ref, EConstr.kind sigma c with
| VarRef id, Var id' -> Names.Id.equal id id'
| ConstRef c, Const (c',_) -> Environ.QConstant.equal env c c'
- | IndRef i, Ind (i', _) -> Names.eq_ind i i'
+ | IndRef i, Ind (i', _) -> Names.Ind.CanOrd.equal i i'
| ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
| _, _ -> false
in
@@ -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 08cb173442..baab41fa26 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -570,7 +570,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
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
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index dc5fd80f9e..43032790e2 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -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/patternops.ml b/pretyping/patternops.ml
index 8c3d624f0f..b5c83b75f9 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
@@ -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 d94cae75bd..9cf7119709 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -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 08303c80d6..4d37c0ef60 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -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'
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:44:28 +0000