aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/eConstr.ml2
-rw-r--r--engine/termops.ml2
-rw-r--r--interp/notation_ops.ml10
-rw-r--r--kernel/constr.ml10
-rw-r--r--kernel/cooking.ml4
-rw-r--r--kernel/names.ml103
-rw-r--r--kernel/names.mli47
-rw-r--r--kernel/nativelambda.ml4
-rw-r--r--library/lib.ml2
-rw-r--r--plugins/cc/ccalgo.ml4
-rw-r--r--plugins/funind/glob_term_to_relation.ml5
-rw-r--r--plugins/funind/glob_termops.ml6
-rw-r--r--pretyping/constr_matching.ml2
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/glob_ops.ml2
-rw-r--r--tactics/equality.ml2
16 files changed, 136 insertions, 71 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 1ac658f123..374cb72753 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -129,7 +129,7 @@ let isRefX sigma x c =
match x, kind sigma c with
| ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c'
| IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i'
- | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+ | ConstructRef i, Construct (i', _) -> Construct.CanOrd.equal i i'
| VarRef id, Var id' -> Id.equal id id'
| _ -> false
diff --git a/engine/termops.ml b/engine/termops.ml
index 031a505ce2..693945d5ac 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1147,7 +1147,7 @@ let compare_constr_univ sigma f cv_pb t1 t2 =
f Reduction.CONV t1 t2 && f cv_pb c1 c2
| Const (c, u), Const (c', u') -> Constant.CanOrd.equal c c'
| Ind (i, _), Ind (i', _) -> Ind.CanOrd.equal i i'
- | Construct (i, _), Construct (i', _) -> eq_constructor i i'
+ | Construct (i, _), Construct (i', _) -> Construct.CanOrd.equal i i'
| _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
let constr_cmp sigma cv_pb t1 t2 =
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 4ca578affd..fe874cd01d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -801,7 +801,7 @@ let rec fold_cases_pattern_eq f x p p' =
let loc = p.CAst.loc in
match DAst.get p, DAst.get p' with
| PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na
- | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' ->
+ | PatCstr (c,l,na), PatCstr (c',l',na') when Construct.CanOrd.equal c c' ->
let x,l = fold_cases_pattern_list_eq f x l l' in
let x,na = f x na na' in
x, DAst.make ?loc @@ PatCstr (c,l,na)
@@ -818,7 +818,7 @@ and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' 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
| _ -> false
@@ -1041,7 +1041,7 @@ let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1
| PatVar na1, PatVar na2 -> match_names metas acc na1 na2
| _, PatVar Anonymous when allow_catchall -> acc
| PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
- when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
+ when Construct.CanOrd.equal c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
List.fold_left2 (match_cases_pattern_binders false metas)
(match_names metas acc na1 na2) patl1 patl2
| _ -> raise No_match
@@ -1391,11 +1391,11 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
match DAst.get a1, a2 with
| r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[])
| PatVar Anonymous, NHole _ -> sigma,(false,0,[])
- | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 ->
+ | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when Construct.CanOrd.equal r1 r2 ->
let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
sigma,(false,0,l)
| PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2)
- when eq_constructor r1 r2 ->
+ when Construct.CanOrd.equal r1 r2 ->
let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
let le2 = List.length l2 in
if le2 > List.length l1
diff --git a/kernel/constr.ml b/kernel/constr.ml
index b453a55d88..d538ad7784 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -355,7 +355,7 @@ let isRefX x c =
match x, kind c with
| ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c'
| IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i'
- | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+ | ConstructRef i, Construct (i', _) -> Construct.CanOrd.equal i i'
| VarRef id, Var id' -> Id.equal id id'
| _ -> false
@@ -957,7 +957,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
Constant.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2
| Ind (c1,u1), Ind (c2,u2) -> Ind.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.IndRef c1, nargs)) u1 u2
| Construct (c1,u1), Construct (c2,u2) ->
- eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2
+ Construct.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2
| Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) ->
eq 0 p1 p2 && eq_invert (eq 0) (leq_universes None) iv1 iv2 && eq 0 c1 c2 && Array.equal (eq 0) bl1 bl2
| Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
@@ -1141,7 +1141,7 @@ let constr_ord_int f t1 t2 =
| Const _, _ -> -1 | _, Const _ -> 1
| Ind (ind1, _u1), Ind (ind2, _u2) -> Ind.CanOrd.compare ind1 ind2
| Ind _, _ -> -1 | _, Ind _ -> 1
- | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2
+ | Construct (ct1,_u1), Construct (ct2,_u2) -> Construct.CanOrd.compare ct1 ct2
| Construct _, _ -> -1 | _, Construct _ -> 1
| Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) ->
let c = f p1 p2 in
@@ -1335,7 +1335,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
| Construct (c,u) ->
let u', hu = sh_instance u in
(Construct (sh_construct c, u'),
- combinesmall 11 (combine (constructor_syntactic_hash c) hu))
+ combinesmall 11 (combine (Construct.SyntacticOrd.hash c) hu))
| Case (ci,p,iv,c,bl) ->
let p, hp = sh_rec p
and iv, hiv = sh_invert iv
@@ -1446,7 +1446,7 @@ let rec hash t =
| Ind (ind,u) ->
combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u))
| Construct (c,u) ->
- combinesmall 11 (combine (constructor_hash c) (Instance.hash u))
+ combinesmall 11 (combine (Construct.CanOrd.hash c) (Instance.hash u))
| Case (_ , p, iv, c, bl) ->
combinesmall 12 (combine4 (hash c) (hash p) (hash_invert iv) (hash_term_array bl))
| Fix (_ln ,(_, tl, bl)) ->
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index cb33bb729c..3707a75157 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -39,13 +39,13 @@ struct
let equal gr1 gr2 = match gr1, gr2 with
| ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
| IndRef i1, IndRef i2 -> Ind.SyntacticOrd.equal i1 i2
- | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
+ | ConstructRef c1, ConstructRef c2 -> Construct.SyntacticOrd.equal c1 c2
| _ -> false
open Hashset.Combine
let hash = function
| ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
| IndRef i -> combinesmall 2 (Ind.SyntacticOrd.hash i)
- | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
+ | ConstructRef c -> combinesmall 3 (Construct.SyntacticOrd.hash c)
end
module RefTable = Hashtbl.Make(RefHash)
diff --git a/kernel/names.ml b/kernel/names.ml
index b36a39ac79..65c602b863 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -648,16 +648,60 @@ struct
end
+module Construct =
+struct
+ (** Designation of a (particular) constructor of a (particular) inductive type. *)
+ type t = Ind.t (* designates the inductive type *)
+ * int (* the index of the constructor
+ BEWARE: indexing starts from 1. *)
+
+ let modpath (ind, _) = Ind.modpath ind
+
+ module CanOrd =
+ struct
+ type nonrec t = t
+ let equal (ind1, j1) (ind2, j2) = Int.equal j1 j2 && Ind.CanOrd.equal ind1 ind2
+ let compare (ind1, j1) (ind2, j2) =
+ let c = Int.compare j1 j2 in
+ if Int.equal c 0 then Ind.CanOrd.compare ind1 ind2 else c
+ let hash (ind, i) =
+ Hashset.Combine.combine (Ind.CanOrd.hash ind) (Int.hash i)
+ end
+
+ module UserOrd =
+ struct
+ type nonrec t = t
+ let equal (ind1, j1) (ind2, j2) =
+ Int.equal j1 j2 && Ind.UserOrd.equal ind1 ind2
+ let compare (ind1, j1) (ind2, j2) =
+ let c = Int.compare j1 j2 in
+ if Int.equal c 0 then Ind.UserOrd.compare ind1 ind2 else c
+ let hash (ind, i) =
+ Hashset.Combine.combine (Ind.UserOrd.hash ind) (Int.hash i)
+ end
+
+ module SyntacticOrd =
+ struct
+ type nonrec t = t
+ let equal (ind1, j1) (ind2, j2) =
+ Int.equal j1 j2 && Ind.SyntacticOrd.equal ind1 ind2
+ let compare (ind1, j1) (ind2, j2) =
+ let c = Int.compare j1 j2 in
+ if Int.equal c 0 then Ind.SyntacticOrd.compare ind1 ind2 else c
+ let hash (ind, i) =
+ Hashset.Combine.combine (Ind.SyntacticOrd.hash ind) (Int.hash i)
+ end
+
+end
+
(** Designation of a (particular) inductive type. *)
type inductive = Ind.t
(** Designation of a (particular) constructor of a (particular) inductive type. *)
-type constructor = inductive (* designates the inductive type *)
- * int (* the index of the constructor
- BEWARE: indexing starts from 1. *)
+type constructor = Construct.t
let ind_modpath = Ind.modpath
-let constr_modpath (ind,_) = ind_modpath ind
+let constr_modpath = Construct.modpath
let ith_mutual_inductive (mind, _) i = (mind, i)
let ith_constructor_of_inductive ind i = (ind, i)
@@ -676,48 +720,27 @@ let ind_hash = Ind.CanOrd.hash
let ind_user_hash = Ind.UserOrd.hash
let ind_syntactic_hash = Ind.SyntacticOrd.hash
-let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
-let eq_user_constructor (ind1, j1) (ind2, j2) =
- Int.equal j1 j2 && eq_user_ind ind1 ind2
-let eq_syntactic_constructor (ind1, j1) (ind2, j2) =
- Int.equal j1 j2 && eq_syntactic_ind ind1 ind2
-
-let constructor_ord (ind1, j1) (ind2, j2) =
- let c = Int.compare j1 j2 in
- if Int.equal c 0 then ind_ord ind1 ind2 else c
-let constructor_user_ord (ind1, j1) (ind2, j2) =
- let c = Int.compare j1 j2 in
- if Int.equal c 0 then ind_user_ord ind1 ind2 else c
-let constructor_syntactic_ord (ind1, j1) (ind2, j2) =
- let c = Int.compare j1 j2 in
- if Int.equal c 0 then ind_syntactic_ord ind1 ind2 else c
-
-let constructor_hash (ind, i) =
- Hashset.Combine.combine (ind_hash ind) (Int.hash i)
-let constructor_user_hash (ind, i) =
- Hashset.Combine.combine (ind_user_hash ind) (Int.hash i)
-let constructor_syntactic_hash (ind, i) =
- Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i)
+let eq_constructor = Construct.CanOrd.equal
+let eq_user_constructor = Construct.UserOrd.equal
+let eq_syntactic_constructor = Construct.SyntacticOrd.equal
+
+let constructor_ord = Construct.CanOrd.compare
+let constructor_user_ord = Construct.UserOrd.compare
+let constructor_syntactic_ord = Construct.SyntacticOrd.compare
+
+let constructor_hash = Construct.CanOrd.hash
+let constructor_user_hash = Construct.UserOrd.hash
+let constructor_syntactic_hash = Construct.SyntacticOrd.hash
module Indset = Set.Make(Ind.CanOrd)
module Indset_env = Set.Make(Ind.UserOrd)
module Indmap = Map.Make(Ind.CanOrd)
module Indmap_env = Map.Make(Ind.UserOrd)
-module ConstructorOrdered = struct
- type t = constructor
- let compare = constructor_ord
-end
-
-module ConstructorOrdered_env = struct
- type t = constructor
- let compare = constructor_user_ord
-end
-
-module Constrset = Set.Make(ConstructorOrdered)
-module Constrset_env = Set.Make(ConstructorOrdered_env)
-module Constrmap = Map.Make(ConstructorOrdered)
-module Constrmap_env = Map.Make(ConstructorOrdered_env)
+module Constrset = Set.Make(Construct.CanOrd)
+module Constrset_env = Set.Make(Construct.UserOrd)
+module Constrmap = Map.Make(Construct.CanOrd)
+module Constrmap_env = Map.Make(Construct.UserOrd)
(** {6 Hash-consing of name objects } *)
diff --git a/kernel/names.mli b/kernel/names.mli
index be53830af5..1ba928a416 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -513,10 +513,39 @@ end
type inductive = Ind.t
-(** Designation of a (particular) constructor of a (particular) inductive type. *)
-type constructor = inductive (* designates the inductive type *)
- * int (* the index of the constructor
- BEWARE: indexing starts from 1. *)
+module Construct :
+sig
+ (** Designation of a (particular) constructor of a (particular) inductive type. *)
+ type t = Ind.t (* designates the inductive type *)
+ * int (* the index of the constructor
+ BEWARE: indexing starts from 1. *)
+
+ val modpath : t -> ModPath.t
+
+ module CanOrd : sig
+ type nonrec t = t
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
+ module UserOrd : sig
+ type nonrec t = t
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
+ module SyntacticOrd : sig
+ type nonrec t = t
+ val compare : t -> t -> int
+ val equal : t -> t -> bool
+ val hash : t -> int
+ end
+
+end
+
+type constructor = Construct.t
module Indset : CSet.S with type elt = inductive
module Constrset : CSet.S with type elt = constructor
@@ -531,6 +560,7 @@ val ind_modpath : inductive -> ModPath.t
[@@ocaml.deprecated "Use the Ind module"]
val constr_modpath : constructor -> ModPath.t
+[@@ocaml.deprecated "Use the Construct module"]
val ith_mutual_inductive : inductive -> int -> inductive
val ith_constructor_of_inductive : inductive -> int -> constructor
@@ -555,14 +585,23 @@ val ind_syntactic_ord : inductive -> inductive -> int
val ind_syntactic_hash : inductive -> int
[@@ocaml.deprecated "Use the Ind module"]
val eq_constructor : constructor -> constructor -> bool
+[@@ocaml.deprecated "Use the Construct module"]
val eq_user_constructor : constructor -> constructor -> bool
+[@@ocaml.deprecated "Use the Construct module"]
val eq_syntactic_constructor : constructor -> constructor -> bool
+[@@ocaml.deprecated "Use the Construct module"]
val constructor_ord : constructor -> constructor -> int
+[@@ocaml.deprecated "Use the Construct module"]
val constructor_hash : constructor -> int
+[@@ocaml.deprecated "Use the Construct module"]
val constructor_user_ord : constructor -> constructor -> int
+[@@ocaml.deprecated "Use the Construct module"]
val constructor_user_hash : constructor -> int
+[@@ocaml.deprecated "Use the Construct module"]
val constructor_syntactic_ord : constructor -> constructor -> int
+[@@ocaml.deprecated "Use the Construct module"]
val constructor_syntactic_hash : constructor -> int
+[@@ocaml.deprecated "Use the Construct module"]
(** {6 Hash-consing } *)
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 99090f0147..e98e97907a 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -433,8 +433,8 @@ module Cache =
module ConstrHash =
struct
type t = constructor
- let equal = eq_constructor
- let hash = constructor_hash
+ let equal = Construct.CanOrd.equal
+ let hash = Construct.CanOrd.hash
end
module ConstrTable = Hashtbl.Make(ConstrHash)
diff --git a/library/lib.ml b/library/lib.ml
index d75177aaa9..fa0a95d366 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -526,7 +526,7 @@ let mp_of_global = let open GlobRef in function
| VarRef id -> !lib_state.path_prefix.Nametab.obj_mp
| ConstRef cst -> Names.Constant.modpath cst
| IndRef ind -> Names.Ind.modpath ind
- | ConstructRef constr -> Names.constr_modpath constr
+ | ConstructRef constr -> Names.Construct.modpath constr
let rec dp_of_mp = function
|Names.MPfile dp -> dp
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 6f5c910297..129b220680 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -145,7 +145,7 @@ let rec term_equal t1 t2 =
| Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2
| Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1},
Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} ->
- Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 (* FIXME check eq? *)
+ Int.equal i1 i2 && Int.equal j1 j2 && Construct.CanOrd.equal c1 c2 (* FIXME check eq? *)
| _ -> false
open Hashset.Combine
@@ -155,7 +155,7 @@ let rec hash_term = function
| Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)
| Eps i -> combine 3 (Id.hash i)
| Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2)
- | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j
+ | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (Construct.CanOrd.hash c) i j
type ccpattern =
PApp of term * ccpattern list (* arguments are reversed *)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6ed61043f9..767a9ec39b 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -332,7 +332,7 @@ let add_pat_variables sigma pat typ env : Environ.env =
let constructors = Inductiveops.get_constructors env indf in
let constructor : Inductiveops.constructor_summary =
List.find
- (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr))
+ (fun cs -> Construct.CanOrd.equal c (fst cs.Inductiveops.cs_cstr))
(Array.to_list constructors)
in
let cs_args_types : types list =
@@ -402,7 +402,8 @@ let rec pattern_to_term_and_type env typ =
let constructors = Inductiveops.get_constructors env indf in
let constructor =
List.find
- (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr)
+ (fun cs ->
+ Construct.CanOrd.equal (fst cs.Inductiveops.cs_cstr) constr)
(Array.to_list constructors)
in
let cs_args_types : types list =
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 8e1331ace9..164a446fe3 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -444,7 +444,8 @@ let rec are_unifiable_aux = function
match (DAst.get l, DAst.get r) with
| PatVar _, _ | _, PatVar _ -> are_unifiable_aux eqs
| PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) ->
- if not (eq_constructor constructor2 constructor1) then raise NotUnifiable
+ if not (Construct.CanOrd.equal constructor2 constructor1) then
+ raise NotUnifiable
else
let eqs' =
try List.combine cpl1 cpl2 @ eqs
@@ -464,7 +465,8 @@ let rec eq_cases_pattern_aux = function
match (DAst.get l, DAst.get r) with
| PatVar _, PatVar _ -> eq_cases_pattern_aux eqs
| PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) ->
- if not (eq_constructor constructor2 constructor1) then raise NotUnifiable
+ if not (Construct.CanOrd.equal constructor2 constructor1) then
+ raise NotUnifiable
else
let eqs' =
try List.combine cpl1 cpl2 @ eqs
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 0200b32ef2..d394bd1288 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -246,7 +246,7 @@ let matches_core env sigma allow_bound_rels
| VarRef id, Var id' -> Names.Id.equal id id'
| 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.eq_constructor c c'
+ | ConstructRef c, Construct (c',u) -> Names.Construct.CanOrd.equal c c'
| _, _ -> false
in
let rec sorec ctx env subst p t =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index baab41fa26..1940668519 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -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
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 43032790e2..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
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 60e2db4dce..486575d229 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -768,7 +768,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
in
(* both sides are fully applied constructors, so either we descend,
or we can discriminate here. *)
- if eq_constructor sp1 sp2 then
+ if Construct.CanOrd.equal sp1 sp2 then
let nparams = inductive_nparams env ind1 in
let params1,rargs1 = List.chop nparams args1 in
let _,rargs2 = List.chop nparams args2 in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:18:43 +0000