Similar introduction of a Construct module in the Names API.

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