Introduce an Ind module in the Names API.

This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.

37 files changed, 188 insertions, 125 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 28d23cc67e..1ac658f123 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -128,7 +128,7 @@ let isRefX sigma x c =
   let open GlobRef in
   match x, kind sigma c with
   | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c'
-  | IndRef i, Ind (i', _) -> eq_ind i i'
+  | IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i'
   | ConstructRef i, Construct (i', _) -> eq_constructor i i'
   | VarRef id, Var id' -> Id.equal id id'
   | _ -> false
diff --git a/engine/termops.ml b/engine/termops.ml
index 3116b03c4f..031a505ce2 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1146,7 +1146,7 @@ let compare_constr_univ sigma f cv_pb t1 t2 =
     | Prod (_,t1,c1), Prod (_,t2,c2) ->
         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', _) -> eq_ind i i'
+    | Ind (i, _), Ind (i', _) -> Ind.CanOrd.equal i i'
     | Construct (i, _), Construct (i', _) -> eq_constructor i i'
     | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 354809252e..4ca578affd 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -58,7 +58,7 @@ match t1, t2 with
     (eq_notation_constr vars) t1 t2
   in
   let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
-    let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
+    let eq (i1, n1) (i2, n2) = Ind.CanOrd.equal i1 i2 && List.equal Name.equal n1 n2 in
     (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
   in
   Option.equal (eq_notation_constr vars) o1 o2 &&
@@ -1418,10 +1418,10 @@ and match_cases_pattern_no_more_args metas sigma a1 a2 =
 
 let match_ind_pattern metas sigma ind pats a2 =
   match a2 with
-  | NRef (GlobRef.IndRef r2) when eq_ind ind r2 ->
+  | NRef (GlobRef.IndRef r2) when Ind.CanOrd.equal ind r2 ->
       sigma,(false,0,pats)
   | NApp (NRef (GlobRef.IndRef r2),l2)
-      when eq_ind ind r2 ->
+      when Ind.CanOrd.equal ind r2 ->
       let le2 = List.length l2 in
       if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats
       then
diff --git a/kernel/constr.ml b/kernel/constr.ml
index fb1e4d12da..b453a55d88 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -354,7 +354,7 @@ let isRefX x c =
   let open GlobRef in
   match x, kind c with
   | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c'
-  | IndRef i, Ind (i', _) -> eq_ind i i'
+  | IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i'
   | ConstructRef i, Construct (i', _) -> eq_constructor i i'
   | VarRef id, Var id' -> Id.equal id id'
   | _ -> false
@@ -955,7 +955,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
   | Const (c1,u1), Const (c2,u2) ->
     (* The args length currently isn't used but may as well pass it. *)
     Constant.CanOrd.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2
-  | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && leq_universes (Some (GlobRef.IndRef 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
   | Case (_,p1,iv1,c1,bl1), Case (_,p2,iv2,c2,bl2) ->
@@ -1139,7 +1139,7 @@ let constr_ord_int f t1 t2 =
     | App _, _ -> -1 | _, App _ -> 1
     | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2
     | Const _, _ -> -1 | _, Const _ -> 1
-    | Ind (ind1, _u1), Ind (ind2, _u2) -> ind_ord ind1 ind2
+    | 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 _, _ -> -1 | _, Construct _ -> 1
@@ -1331,7 +1331,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
       | Ind (ind,u) ->
         let u', hu = sh_instance u in
         (Ind (sh_ind ind, u'),
-         combinesmall 10 (combine (ind_syntactic_hash ind) hu))
+         combinesmall 10 (combine (Ind.SyntacticOrd.hash ind) hu))
       | Construct (c,u) ->
         let u', hu = sh_instance u in
         (Construct (sh_construct c, u'),
@@ -1444,7 +1444,7 @@ let rec hash t =
     | Const (c,u) ->
       combinesmall 9 (combine (Constant.CanOrd.hash c) (Instance.hash u))
     | Ind (ind,u) ->
-      combinesmall 10 (combine (ind_hash ind) (Instance.hash u))
+      combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u))
     | Construct (c,u) ->
       combinesmall 11 (combine (constructor_hash c) (Instance.hash u))
     | Case (_ , p, iv, c, bl) ->
@@ -1503,7 +1503,7 @@ struct
     let h3 = Array.fold_left hash_bool_list 0 info.cstr_tags in
     combine3 h1 h2 h3
   let hash ci =
-    let h1 = ind_hash ci.ci_ind in
+    let h1 = Ind.CanOrd.hash ci.ci_ind in
     let h2 = Int.hash ci.ci_npar in
     let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in
     let h4 = Array.fold_left combine 0 ci.ci_cstr_nargs in
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index fdcf44c943..cb33bb729c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -38,13 +38,13 @@ struct
   type t = my_global_reference
   let equal gr1 gr2 = match gr1, gr2 with
   | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2
-  | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2
+  | IndRef i1, IndRef i2 -> Ind.SyntacticOrd.equal i1 i2
   | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2
   | _ -> false
   open Hashset.Combine
   let hash = function
   | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c)
-  | IndRef i -> combinesmall 2 (ind_syntactic_hash i)
+  | IndRef i -> combinesmall 2 (Ind.SyntacticOrd.hash i)
   | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c)
 end
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index ee90ad382b..8de7123fee 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -157,7 +157,7 @@ let hcons_const_body cb =
 
 (** {6 Inductive types } *)
 let eq_nested_type t1 t2 = match t1, t2 with
-| NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2
+| NestedInd ind1, NestedInd ind2 -> Names.Ind.CanOrd.equal ind1 ind2
 | NestedInd _, _ -> false
 | NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2
 | NestedPrimitive _, _ -> false
@@ -165,7 +165,7 @@ let eq_nested_type t1 t2 = match t1, t2 with
 let eq_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> true
 | Norec, _ -> false
-| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
+| Mrec i1, Mrec i2 -> Names.Ind.CanOrd.equal i1 i2
 | Mrec _, _ -> false
 | Nested ty1, Nested ty2 -> eq_nested_type ty1 ty2
 | Nested _, _ -> false
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2b1a295620..e34b3c0b47 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -404,7 +404,7 @@ let type_case_branches env (pind,largs) pj c =
 let check_case_info env (indsp,u) r ci =
   let (mib,mip as spec) = lookup_mind_specif env indsp in
   if
-    not (eq_ind indsp ci.ci_ind) ||
+    not (Ind.CanOrd.equal indsp ci.ci_ind) ||
     not (Int.equal mib.mind_nparams ci.ci_npar) ||
     not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) ||
     not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) ||
@@ -467,9 +467,9 @@ let inter_recarg r1 r2 = match r1, r2 with
 | Norec, _ -> None
 | Mrec i1, Mrec i2
 | Nested (NestedInd i1), Nested (NestedInd i2)
-| Mrec i1, (Nested (NestedInd i2)) -> if Names.eq_ind i1 i2 then Some r1 else None
+| Mrec i1, (Nested (NestedInd i2)) -> if Names.Ind.CanOrd.equal i1 i2 then Some r1 else None
 | Mrec _, _ -> None
-| Nested (NestedInd i1), Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None
+| Nested (NestedInd i1), Mrec i2 -> if Names.Ind.CanOrd.equal i1 i2 then Some r2 else None
 | Nested (NestedInd _), _ -> None
 | Nested (NestedPrimitive c1), Nested (NestedPrimitive c2) ->
   if Names.Constant.CanOrd.equal c1 c2 then Some r1 else None
@@ -556,7 +556,7 @@ let lookup_subterms env ind =
 
 let match_inductive ind ra =
   match ra with
-    | Mrec i | Nested (NestedInd i) -> eq_ind ind i
+    | Mrec i | Nested (NestedInd i) -> Ind.CanOrd.equal ind i
     | Norec | Nested (NestedPrimitive _) -> false
 
 (* In {match c as z in ci y_s return P with |C_i x_s => t end}
@@ -667,7 +667,7 @@ let get_recargs_approx env tree ind args =
        (* When the inferred tree allows it, we consider that we have a potential
        nested inductive type *)
        begin match dest_recarg tree with
-             | Nested (NestedInd kn') | Mrec kn' when eq_ind (fst ind_kn) kn' ->
+             | Nested (NestedInd kn') | Mrec kn' when Ind.CanOrd.equal (fst ind_kn) kn' ->
                build_recargs_nested ienv tree (ind_kn, largs)
              | _ -> mk_norec
        end
diff --git a/kernel/names.ml b/kernel/names.ml
index f7658df355..b36a39ac79 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -600,18 +600,63 @@ module Mindmap = HMap.Make(MutInd.CanOrd)
 module Mindset = Mindmap.Set
 module Mindmap_env = HMap.Make(MutInd.UserOrd)
 
+module Ind =
+struct
+  (** Designation of a (particular) inductive type. *)
+  type t = MutInd.t      (* the name of the inductive type *)
+        * int           (* the position of this inductive type
+                                    within the block of mutually-recursive inductive types.
+                                    BEWARE: indexing starts from 0. *)
+  let modpath (mind, _) = MutInd.modpath mind
+
+  module CanOrd =
+  struct
+    type nonrec t = t
+    let equal (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.CanOrd.equal m1 m2
+    let compare (m1, i1) (m2, i2) =
+      let c = Int.compare i1 i2 in
+      if Int.equal c 0 then MutInd.CanOrd.compare m1 m2 else c
+    let hash (m, i) =
+      Hashset.Combine.combine (MutInd.CanOrd.hash m) (Int.hash i)
+  end
+
+  module UserOrd =
+  struct
+    type nonrec t = t
+    let equal (m1, i1) (m2, i2) =
+      Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2
+    let compare (m1, i1) (m2, i2) =
+      let c = Int.compare i1 i2 in
+      if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c
+    let hash (m, i) =
+      Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i)
+  end
+
+  module SyntacticOrd =
+  struct
+    type nonrec t = t
+    let equal (m1, i1) (m2, i2) =
+      Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2
+
+    let compare (m1, i1) (m2, i2) =
+      let c = Int.compare i1 i2 in
+      if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c
+
+    let hash (m, i) =
+      Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i)
+  end
+
+end
+
 (** Designation of a (particular) inductive type. *)
-type inductive = MutInd.t      (* the name of the inductive type *)
-               * int           (* the position of this inductive type
-                                  within the block of mutually-recursive inductive types.
-                                  BEWARE: indexing starts from 0. *)
+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. *)
 
-let ind_modpath (mind,_) = MutInd.modpath mind
+let ind_modpath = Ind.modpath
 let constr_modpath (ind,_) = ind_modpath ind
 
 let ith_mutual_inductive (mind, _) i = (mind, i)
@@ -619,28 +664,17 @@ let ith_constructor_of_inductive ind i = (ind, i)
 let inductive_of_constructor (ind, _i) = ind
 let index_of_constructor (_ind, i) = i
 
-let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2
-let eq_user_ind (m1, i1) (m2, i2) =
-  Int.equal i1 i2 && MutInd.UserOrd.equal m1 m2
-let eq_syntactic_ind (m1, i1) (m2, i2) =
-  Int.equal i1 i2 && MutInd.SyntacticOrd.equal m1 m2
-
-let ind_ord (m1, i1) (m2, i2) =
-  let c = Int.compare i1 i2 in
-  if Int.equal c 0 then MutInd.CanOrd.compare m1 m2 else c
-let ind_user_ord (m1, i1) (m2, i2) =
-  let c = Int.compare i1 i2 in
-  if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c
-let ind_syntactic_ord (m1, i1) (m2, i2) =
-  let c = Int.compare i1 i2 in
-  if Int.equal c 0 then MutInd.SyntacticOrd.compare m1 m2 else c
-
-let ind_hash (m, i) =
-  Hashset.Combine.combine (MutInd.hash m) (Int.hash i)
-let ind_user_hash (m, i) =
-  Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i)
-let ind_syntactic_hash (m, i) =
-  Hashset.Combine.combine (MutInd.SyntacticOrd.hash m) (Int.hash i)
+let eq_ind = Ind.CanOrd.equal
+let eq_user_ind = Ind.UserOrd.equal
+let eq_syntactic_ind = Ind.SyntacticOrd.equal
+
+let ind_ord = Ind.CanOrd.compare
+let ind_user_ord = Ind.UserOrd.compare
+let ind_syntactic_ord = Ind.SyntacticOrd.compare
+
+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) =
@@ -665,20 +699,10 @@ let constructor_user_hash (ind, i) =
 let constructor_syntactic_hash (ind, i) =
   Hashset.Combine.combine (ind_syntactic_hash ind) (Int.hash i)
 
-module InductiveOrdered = struct
-  type t = inductive
-  let compare = ind_ord
-end
-
-module InductiveOrdered_env = struct
-  type t = inductive
-  let compare = ind_user_ord
-end
-
-module Indset = Set.Make(InductiveOrdered)
-module Indset_env = Set.Make(InductiveOrdered_env)
-module Indmap = Map.Make(InductiveOrdered)
-module Indmap_env = Map.Make(InductiveOrdered_env)
+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
diff --git a/kernel/names.mli b/kernel/names.mli
index 76be6ca105..be53830af5 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -479,11 +479,39 @@ module Mindset : CSig.SetS with type elt = MutInd.t
 module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset
 module Mindmap_env : CMap.ExtS with type key = MutInd.t
 
-(** Designation of a (particular) inductive type. *)
-type inductive = MutInd.t      (* the name of the inductive type *)
-               * int           (* the position of this inductive type
-                                  within the block of mutually-recursive inductive types.
-                                  BEWARE: indexing starts from 0. *)
+module Ind :
+sig
+  (** Designation of a (particular) inductive type. *)
+  type t = MutInd.t      (* the name of the inductive type *)
+         * int           (* the position of this inductive type
+                                    within the block of mutually-recursive inductive types.
+                                    BEWARE: indexing starts from 0. *)
+  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 inductive = Ind.t
 
 (** Designation of a (particular) constructor of a (particular) inductive type. *)
 type constructor = inductive   (* designates the inductive type *)
@@ -500,6 +528,8 @@ module Indmap_env : CMap.ExtS with type key = inductive and module Set := Indset
 module Constrmap_env : CMap.ExtS with type key = constructor and module Set := Constrset_env
 
 val ind_modpath : inductive -> ModPath.t
+[@@ocaml.deprecated "Use the Ind module"]
+
 val constr_modpath : constructor -> ModPath.t
 
 val ith_mutual_inductive : inductive -> int -> inductive
@@ -507,14 +537,23 @@ val ith_constructor_of_inductive : inductive -> int -> constructor
 val inductive_of_constructor : constructor -> inductive
 val index_of_constructor : constructor -> int
 val eq_ind : inductive -> inductive -> bool
+[@@ocaml.deprecated "Use the Ind module"]
 val eq_user_ind : inductive -> inductive -> bool
+[@@ocaml.deprecated "Use the Ind module"]
 val eq_syntactic_ind : inductive -> inductive -> bool
+[@@ocaml.deprecated "Use the Ind module"]
 val ind_ord : inductive -> inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
 val ind_hash : inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
 val ind_user_ord : inductive -> inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
 val ind_user_hash : inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
 val ind_syntactic_ord : inductive -> inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
 val ind_syntactic_hash : inductive -> int
+[@@ocaml.deprecated "Use the Ind module"]
 val eq_constructor : constructor -> constructor -> bool
 val eq_user_constructor : constructor -> constructor -> bool
 val eq_syntactic_constructor : constructor -> constructor -> bool
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 9314203e04..b5c4d6416a 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -65,11 +65,11 @@ type gname =
 let eq_gname gn1 gn2 =
   match gn1, gn2 with
   | Gind (s1, ind1), Gind (s2, ind2) ->
-     String.equal s1 s2 && eq_ind ind1 ind2
+     String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2
   | Gconstant (s1, c1), Gconstant (s2, c2) ->
       String.equal s1 s2 && Constant.CanOrd.equal c1 c2
   | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) ->
-    String.equal s1 s2 && eq_ind ind1 ind2 && Int.equal i1 i2
+    String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2 && Int.equal i1 i2
   | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2
   | Gcase (Some l1, i1), Gcase (Some l2, i2) -> Int.equal i1 i2 && Label.equal l1 l2
   | Gpred (None, i1), Gpred (None, i2) -> Int.equal i1 i2
@@ -96,7 +96,7 @@ open Hashset.Combine
 
 let gname_hash gn = match gn with
 | Gind (s, ind) ->
-   combinesmall 1 (combine (String.hash s) (ind_hash ind))
+   combinesmall 1 (combine (String.hash s) (Ind.CanOrd.hash ind))
 | Gconstant (s, c) ->
    combinesmall 2 (combine (String.hash s) (Constant.CanOrd.hash c))
 | Gcase (l, i) -> combinesmall 3 (combine (Option.hash Label.hash l) (Int.hash i))
@@ -107,7 +107,7 @@ let gname_hash gn = match gn with
 | Ginternal s -> combinesmall 8 (String.hash s)
 | Grel i -> combinesmall 9 (Int.hash i)
 | Gnamed id -> combinesmall 10 (Id.hash id)
-| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (ind_hash p) i))
+| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (Ind.CanOrd.hash p) i))
 
 let case_ctr = ref (-1)
 
@@ -150,11 +150,11 @@ let eq_symbol sy1 sy2 =
   | SymbName n1, SymbName n2 -> Name.equal n1 n2
   | SymbConst kn1, SymbConst kn2 -> Constant.CanOrd.equal kn1 kn2
   | SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2
-  | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2
+  | SymbInd ind1, SymbInd ind2 -> Ind.CanOrd.equal ind1 ind2
   | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2
   | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2
   | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2
-  | SymbProj (i1, k1), SymbProj (i2, k2) -> eq_ind i1 i2 && Int.equal k1 k2
+  | SymbProj (i1, k1), SymbProj (i2, k2) -> Ind.CanOrd.equal i1 i2 && Int.equal k1 k2
   | _, _ -> false
 
 let hash_symbol symb =
@@ -164,11 +164,11 @@ let hash_symbol symb =
   | SymbName name -> combinesmall 3 (Name.hash name)
   | SymbConst c -> combinesmall 4 (Constant.CanOrd.hash c)
   | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw)
-  | SymbInd ind -> combinesmall 6 (ind_hash ind)
+  | SymbInd ind -> combinesmall 6 (Ind.CanOrd.hash ind)
   | SymbMeta m -> combinesmall 7 m
   | SymbEvar evk -> combinesmall 8 (Evar.hash evk)
   | SymbLevel l -> combinesmall 9 (Univ.Level.hash l)
-  | SymbProj (i, k) -> combinesmall 10 (combine (ind_hash i) k)
+  | SymbProj (i, k) -> combinesmall 10 (combine (Ind.CanOrd.hash i) k)
 
 module HashedTypeSymbol = struct
   type t = symbol
@@ -438,7 +438,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
       eq_mllam_branches gn1 gn2 n env1 env2 br1 br2
   | MLconstruct (pf1, ind1, tag1, args1), MLconstruct (pf2, ind2, tag2, args2) ->
       String.equal pf1 pf2 &&
-      eq_ind ind1 ind2 &&
+      Ind.CanOrd.equal ind1 ind2 &&
       Int.equal tag1 tag2 &&
       Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2
   | MLint i1, MLint i2 ->
@@ -457,7 +457,7 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
       Array.equal (eq_mllambda gn1 gn2 n env1 env2) arr1 arr2
 
   | MLisaccu (s1, ind1, ml1), MLisaccu (s2, ind2, ml2) ->
-    String.equal s1 s2 && eq_ind ind1 ind2 &&
+    String.equal s1 s2 && Ind.CanOrd.equal ind1 ind2 &&
     eq_mllambda gn1 gn2 n env1 env2 ml1 ml2
   | (MLlocal _ | MLglobal _ | MLprimitive _ | MLlam _ | MLletrec _ | MLlet _ |
     MLapp _ | MLif _ | MLmatch _ | MLconstruct _ | MLint _ | MLuint _ |
@@ -527,7 +527,7 @@ let rec hash_mllambda gn n env t =
       combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br)
   | MLconstruct (pf, ind, tag, args) ->
       let hpf = String.hash pf in
-      let hcs = ind_hash ind in
+      let hcs = Ind.CanOrd.hash ind in
       let htag = Int.hash tag in
       combinesmall 10 (hash_mllambda_array gn n env (combine3 hpf hcs htag) args)
   | MLint i ->
@@ -545,7 +545,7 @@ let rec hash_mllambda gn n env t =
   | MLarray arr ->
       combinesmall 15 (hash_mllambda_array gn n env 1 arr)
   | MLisaccu (s, ind, c) ->
-      combinesmall 16 (combine (String.hash s) (combine (ind_hash ind) (hash_mllambda gn n env c)))
+      combinesmall 16 (combine (String.hash s) (combine (Ind.CanOrd.hash ind) (hash_mllambda gn n env c)))
   | MLfloat f ->
       combinesmall 17 (Float64.hash f)
 
@@ -689,7 +689,7 @@ let eq_global g1 g2 =
       eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2
   | Gopen s1, Gopen s2 -> String.equal s1 s2
   | Gtype (ind1, arr1), Gtype (ind2, arr2) ->
-    eq_ind ind1 ind2 &&
+    Ind.CanOrd.equal ind1 ind2 &&
     Array.equal (fun (tag1,ar1) (tag2,ar2) -> Int.equal tag1 tag2 && Int.equal ar1 ar2) arr1 arr2
   | Gcomment s1, Gcomment s2 -> String.equal s1 s2
   | _, _ -> false
@@ -720,7 +720,7 @@ let hash_global g =
     let hash_aux acc (tag,ar) =
       combine3 acc (Int.hash tag) (Int.hash ar)
     in
-    combinesmall 6 (combine (ind_hash ind) (Array.fold_left hash_aux 0 arr))
+    combinesmall 6 (combine (Ind.CanOrd.hash ind) (Array.fold_left hash_aux 0 arr))
   | Gcomment s -> combinesmall 7 (String.hash s)
 
 let global_stack = ref ([] : global list)
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 00418009c7..76215b4386 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -80,7 +80,7 @@ and conv_atom env pb lvl a1 a2 cu =
     | Arel i1, Arel i2 ->
         if Int.equal i1 i2 then cu else raise NotConvertible
     | Aind (ind1,u1), Aind (ind2,u2) ->
-       if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
+       if Ind.CanOrd.equal ind1 ind2 then convert_instances ~flex:false u1 u2 cu
        else raise NotConvertible
     | Aconstant (c1,u1), Aconstant (c2,u2) ->
        if Constant.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
@@ -90,7 +90,7 @@ and conv_atom env pb lvl a1 a2 cu =
     | Avar id1, Avar id2 ->
         if Id.equal id1 id2 then cu else raise NotConvertible
     | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
-        if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
+        if not (Ind.CanOrd.equal a1.asw_ind a2.asw_ind) then raise NotConvertible;
         let cu = conv_accu env CONV lvl ac1 ac2 cu in
         let tbl = a1.asw_reloc in
         let len = Array.length tbl in
@@ -124,7 +124,7 @@ and conv_atom env pb lvl a1 a2 cu =
        let v = mk_rel_accu lvl in
        conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
     | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) ->
-       if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible
+       if not (Ind.CanOrd.equal ind1 ind2 && Int.equal i1 i2) then raise NotConvertible
        else conv_accu env CONV lvl ac1 ac2 cu
     | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
     | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 05c98e4b87..bd6241ae67 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -36,13 +36,13 @@ type annot_sw = {
 
 (* We compare only what is relevant for generation of ml code *)
 let eq_annot_sw asw1 asw2 =
-  eq_ind asw1.asw_ind asw2.asw_ind &&
+  Ind.CanOrd.equal asw1.asw_ind asw2.asw_ind &&
   String.equal asw1.asw_prefix asw2.asw_prefix
 
 open Hashset.Combine
 
 let hash_annot_sw asw =
-  combine (ind_hash asw.asw_ind) (String.hash asw.asw_prefix)
+  combine (Ind.CanOrd.hash asw.asw_ind) (String.hash asw.asw_prefix)
 
 type sort_annot = string * int
 
diff --git a/kernel/primred.ml b/kernel/primred.ml
index 17e5a89b74..f0b4d6d362 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -16,7 +16,7 @@ let check_same_types typ c1 c2 =
   then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
 
 let check_same_inds ind i1 i2 =
-  if not (eq_ind i1 i2)
+  if not (Ind.CanOrd.equal i1 i2)
   then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2))
 
 let add_retroknowledge retro action =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 8eb1c10f70..5589ae3483 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -568,7 +568,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
     | (FInd (ind1,u1 as pind1), FInd (ind2,u2 as pind2)) ->
-      if eq_ind ind1 ind2 then
+      if Ind.CanOrd.equal ind1 ind2 then
         if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
           let cuniv = convert_instances ~flex:false u1 u2 cuniv in
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -588,7 +588,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) ->
-      if Int.equal j1 j2 && eq_ind ind1 ind2 then
+      if Int.equal j1 j2 && Ind.CanOrd.equal ind1 ind2 then
         if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
           let cuniv = convert_instances ~flex:false u1 u2 cuniv in
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -669,7 +669,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         else raise NotConvertible
 
     | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) ->
-      (if not (eq_ind ci1.ci_ind ci2.ci_ind) then raise NotConvertible);
+      (if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible);
       let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in
       let ccnv = ccnv CONV l2r infos el1 el2 in
       let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in
@@ -711,7 +711,7 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
                 let cu2 = f fx1 fx2 cu1 in
                 cmp_rec a1 a2 cu2
             | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) ->
-                if not (eq_ind ci1.ci_ind ci2.ci_ind) then
+                if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then
                   raise NotConvertible;
                 let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in
                 convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index f86c12e1f1..85e24f87b7 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -413,7 +413,7 @@ let type_of_projection env p c ct =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (make_judge c ct)
   in
-  assert(eq_ind (Projection.inductive p) ind);
+  assert(Ind.CanOrd.equal (Projection.inductive p) ind);
   let ty = Vars.subst_instance_constr u pty in
   substl (c :: CList.rev args) ty
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 2de902c827..1432fb9310 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -95,7 +95,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
 (*  Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *)
   match a1, a2 with
   | Aind ((mi,_i) as ind1) , Aind ind2 ->
-    if eq_ind ind1 ind2 && compare_stack stk1 stk2 then
+    if Ind.CanOrd.equal ind1 ind2 && compare_stack stk1 stk2 then
       let ulen = Univ.AUContext.size (Environ.mind_context env mi) in
       if ulen = 0 then
         conv_stack env k stk1 stk2 cu
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 28a7abc7c6..7b4101b9d0 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -96,7 +96,7 @@ let hash_structured_values (v : structured_values) =
 let eq_structured_constant c1 c2 = match c1, c2 with
 | Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2
 | Const_sort _, _ -> false
-| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
+| Const_ind i1, Const_ind i2 -> Ind.CanOrd.equal i1 i2
 | Const_ind _, _ -> false
 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
 | Const_b0 _, _ -> false
@@ -113,7 +113,7 @@ let hash_structured_constant c =
   let open Hashset.Combine in
   match c with
   | Const_sort s -> combinesmall 1 (Sorts.hash s)
-  | Const_ind i -> combinesmall 2 (ind_hash i)
+  | Const_ind i -> combinesmall 2 (Ind.CanOrd.hash i)
   | Const_b0 t -> combinesmall 3 (Int.hash t)
   | Const_univ_level l -> combinesmall 4 (Univ.Level.hash l)
   | Const_val v -> combinesmall 5 (hash_structured_values v)
diff --git a/library/coqlib.ml b/library/coqlib.ml
index b374ecbca0..82d1ecacb5 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -45,7 +45,7 @@ let has_ref s = CString.Map.mem s !table
 
 let check_ind_ref s ind =
   match CString.Map.find s !table with
-  | GlobRef.IndRef r -> eq_ind r ind
+  | GlobRef.IndRef r -> Ind.CanOrd.equal r ind
   | _ -> false
   | exception Not_found -> false
 
diff --git a/library/lib.ml b/library/lib.ml
index 830777003b..d75177aaa9 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -525,7 +525,7 @@ let init () =
 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
+  | IndRef ind -> Names.Ind.modpath ind
   | ConstructRef constr -> Names.constr_modpath constr
 
 let rec dp_of_mp = function
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 23f8fe04a3..ac2058ba1b 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -115,7 +115,7 @@ module Bool = struct
     | Case (info, r, _iv, arg, pats) ->
       let is_bool =
         let i = info.ci_ind in
-        Names.eq_ind i (Lazy.force ind)
+        Names.Ind.CanOrd.equal i (Lazy.force ind)
       in
       if is_bool then
         Ifb ((aux arg), (aux pats.(0)), (aux pats.(1)))
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index b1ce10985a..21ec80abbc 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -685,7 +685,7 @@ let is_regular_match br =
         | _ -> raise Impossible
       in
       let is_ref i tr = match get_r tr with
-      | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1)
+      | GlobRef.ConstructRef (ind', j) -> Ind.CanOrd.equal ind ind' && Int.equal j (i + 1)
       | _ -> false
       in
       Array.for_all_i is_ref 0 br
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index d464ec4c06..61f90608b1 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -100,7 +100,7 @@ let rec make_form env sigma atom_env term =
   | Cast(a,_,_) ->
     make_form env sigma atom_env a
   | Ind (ind, _) ->
-    if Names.eq_ind ind (fst (Lazy.force li_False)) then
+    if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_False)) then
       Bot
     else
       make_atom atom_env (normalize term)
@@ -108,11 +108,11 @@ let rec make_form env sigma atom_env term =
     begin
       try
         let ind, _ = destInd sigma hd in
-        if Names.eq_ind ind (fst (Lazy.force li_and)) then
+        if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_and)) then
           let fa = make_form env sigma atom_env argv.(0) in
           let fb = make_form env sigma atom_env argv.(1) in
           Conjunct (fa,fb)
-        else if Names.eq_ind ind (fst (Lazy.force li_or)) then
+        else if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_or)) then
           let fa = make_form env sigma atom_env argv.(0) in
           let fb = make_form env sigma atom_env argv.(1) in
           Disjunct (fa,fb)
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'
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 49437a2aef..9a55cabc86 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -193,7 +193,7 @@ let head_in indl t gl =
   let sigma = Tacmach.New.project gl in
   try
     let ity,_ = extract_mrectype sigma t in
-    List.exists (fun i -> eq_ind (fst i) (fst ity)) indl
+    List.exists (fun i -> Ind.CanOrd.equal (fst i) (fst ity)) indl
   with Not_found -> false
 
 let decompose_these c l =
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index fee9dd1b96..df07dcbca7 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -91,7 +91,7 @@ struct
     | DArray (t,def,ty) -> DArray(Array.map f t, f def, f ty)
 
   let compare_ci ci1 ci2 =
-    let c = ind_ord ci1.ci_ind ci2.ci_ind in
+    let c = Ind.CanOrd.compare ci1.ci_ind ci2.ci_ind in
     if c = 0 then
       let c = Int.compare ci1.ci_npar ci2.ci_npar in
       if c = 0 then
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 475d4e9af9..f715459616 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -496,7 +496,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
           let u,v = try destruct_ind env sigma tt1
           (* trick so that the good sequence is returned*)
                 with e when CErrors.noncritical e -> indu,[||]
-          in if eq_ind (fst u) ind
+          in if Ind.CanOrd.equal (fst u) ind
              then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
              else (
                find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 5f7eb78a40..bef9e29ac2 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -656,7 +656,7 @@ let explain_evar_not_found env sigma id =
 
 let explain_wrong_case_info env (ind,u) ci =
   let pi = pr_inductive env ind in
-  if eq_ind ci.ci_ind ind then
+  if Ind.CanOrd.equal ci.ci_ind ind then
     str "Pattern-matching expression on an object of inductive type" ++
     spc () ++ pi ++ spc () ++ str "has invalid information."
   else
@@ -1232,7 +1232,7 @@ let error_not_allowed_dependent_analysis env isrec i =
   pr_inductive env i ++ str "."
 
 let error_not_mutual_in_scheme env ind ind' =
-  if eq_ind ind ind' then
+  if Ind.CanOrd.equal ind ind' then
     str "The inductive type " ++ pr_inductive env ind ++
     str " occurs twice."
   else
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml
index 79468627de..af72c01758 100644
--- a/vernac/recLemmas.ml
+++ b/vernac/recLemmas.ml
@@ -70,7 +70,7 @@ let find_mutually_recursive_statements sigma thms =
       | [], _::_ ->
           let () = match same_indccl with
           | ind :: _ ->
-            if List.distinct_f Names.ind_ord (List.map pi1 ind)
+            if List.distinct_f Names.Ind.CanOrd.compare (List.map pi1 ind)
             then
               Flags.if_verbose Feedback.msg_info
                 (Pp.strbrk