From 8f16b1c5b97411b7ea88279699f0f410f1c77723 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Sep 2020 11:04:21 +0200
Subject: Introduce a dummy name quotient API.

For now it does not do anything but eventually it should be used to replace
the reliance on canonical names for dual kerpairs such as e.g. constants and
inductive types.
---
 kernel/environ.ml  | 33 +++++++++++++++++++++++++++++++++
 kernel/environ.mli | 35 +++++++++++++++++++++++++++++++++++
 2 files changed, 68 insertions(+)

diff --git a/kernel/environ.ml b/kernel/environ.ml
index dec9e1deb8..ac7775b89c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -832,3 +832,36 @@ let set_retroknowledge env r = { env with retroknowledge = r }
 let set_native_symbols env native_symbols = { env with native_symbols }
 let add_native_symbols dir syms env =
   { env with native_symbols = DPmap.add dir syms env.native_symbols }
+
+module QConstant =
+struct
+  type t = Constant.t
+  let equal _env c1 c2 = Constant.CanOrd.equal c1 c2
+  let compare _env c1 c2 = Constant.CanOrd.compare c1 c2
+  let hash _env c = Constant.CanOrd.hash c
+  let canonical _env c = (Constant.canonical c)
+end
+
+module QMutInd =
+struct
+  type t = MutInd.t
+  let equal _env c1 c2 = MutInd.CanOrd.equal c1 c2
+  let compare _env c1 c2 = MutInd.CanOrd.compare c1 c2
+  let hash _env c = MutInd.CanOrd.hash c
+  let canonical _env c = (MutInd.canonical c)
+end
+
+module QProjection =
+struct
+  type t = Projection.t
+  let equal _env c1 c2 = Projection.CanOrd.equal c1 c2
+  let compare _env c1 c2 = Projection.CanOrd.compare c1 c2
+  let hash _env c = Projection.CanOrd.hash c
+  module Repr =
+  struct
+    type t = Projection.Repr.t
+    let equal _env c1 c2 = Projection.Repr.CanOrd.equal c1 c2
+    let compare _env c1 c2 = Projection.Repr.CanOrd.compare c1 c2
+    let hash _env c = Projection.Repr.CanOrd.hash c
+  end
+end
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f443ba38e1..370443857c 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -284,6 +284,41 @@ val template_polymorphic_ind : inductive -> env -> bool
 val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
 val template_polymorphic_pind : pinductive -> env -> bool
 
+(** {6 Name quotients} *)
+
+module QConstant :
+sig
+  type t = Constant.t
+  val equal : env -> t -> t -> bool
+  val compare : env -> t -> t -> int
+  val hash : env -> t -> int
+  val canonical : env -> t -> KerName.t
+end
+
+module QMutInd :
+sig
+  type t = MutInd.t
+  val equal : env -> t -> t -> bool
+  val compare : env -> t -> t -> int
+  val hash : env -> t -> int
+  val canonical : env -> t -> KerName.t
+end
+
+module QProjection :
+sig
+  type t = Projection.t
+  val equal : env -> t -> t -> bool
+  val compare : env -> t -> t -> int
+  val hash : env -> t -> int
+  module Repr :
+  sig
+    type t = Projection.Repr.t
+    val equal : env -> t -> t -> bool
+    val compare : env -> t -> t -> int
+    val hash : env -> t -> int
+  end
+end
+
 (** {5 Modules } *)
 
 val add_modtype : module_type_body -> env -> env
-- 
cgit v1.2.3


From 2b91a8989687e152f7120aa6c907ffeba8495bab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Sep 2020 10:44:51 +0200
Subject: Deprecate the non-qualified equality functions on kerpairs.

This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
---
 checker/checkInductive.ml                      |  2 +-
 engine/eConstr.ml                              |  4 ++--
 engine/termops.ml                              |  2 +-
 kernel/constr.ml                               |  6 +++---
 kernel/declareops.ml                           |  2 +-
 kernel/inductive.ml                            |  6 +++---
 kernel/names.ml                                |  1 +
 kernel/names.mli                               | 16 +++++++++++-----
 kernel/nativecode.ml                           |  8 ++++----
 kernel/nativeconv.ml                           |  2 +-
 kernel/primred.ml                              |  2 +-
 kernel/reduction.ml                            |  2 +-
 kernel/subtyping.ml                            |  2 +-
 kernel/vmemitcodes.ml                          |  4 ++--
 kernel/vmvalues.ml                             |  4 ++--
 plugins/extraction/extraction.ml               |  2 +-
 plugins/extraction/table.ml                    |  2 +-
 plugins/funind/functional_principles_proofs.ml |  2 +-
 plugins/funind/functional_principles_types.ml  |  4 ++--
 plugins/funind/gen_principle.ml                |  7 ++++---
 plugins/funind/invfun.ml                       |  3 ++-
 plugins/ltac/rewrite.ml                        |  2 +-
 plugins/ssrmatching/ssrmatching.ml             |  6 +++---
 pretyping/constr_matching.ml                   |  6 +++---
 pretyping/evarconv.ml                          |  6 +++---
 pretyping/evardefine.ml                        |  2 +-
 pretyping/indrec.ml                            |  2 +-
 pretyping/tacred.ml                            |  6 +++---
 pretyping/unification.ml                       |  8 ++++----
 tactics/cbn.ml                                 |  2 +-
 tactics/tactics.ml                             |  2 +-
 vernac/auto_ind_decl.ml                        |  7 ++++---
 vernac/declare.ml                              |  2 +-
 vernac/indschemes.ml                           |  2 +-
 vernac/recLemmas.ml                            |  2 +-
 35 files changed, 74 insertions(+), 64 deletions(-)

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index ef606c9a75..7bb714aa17 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -104,7 +104,7 @@ let check_kelim k1 k2 = Sorts.family_leq k1 k2
 let eq_nested_types ty1 ty2 = match ty1, ty2 with
 | NestedInd ind1, NestedInd ind2 -> eq_ind_chk ind1 ind2
 | NestedInd _, _ -> false
-| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2
+| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2
 | NestedPrimitive _, _ -> false
 
 let eq_recarg a1 a2 = match a1, a2 with
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 36297fe243..28d23cc67e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -127,7 +127,7 @@ let isRef sigma c = match kind sigma c with
 let isRefX sigma x c =
   let open GlobRef in
   match x, kind sigma c with
-  | ConstRef c, Const (c', _) -> Constant.equal c c'
+  | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c'
   | IndRef i, Ind (i', _) -> eq_ind i i'
   | ConstructRef i, Construct (i', _) -> eq_constructor i i'
   | VarRef id, Var id' -> Id.equal id id'
@@ -514,7 +514,7 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n =
   | Proj (p, c), App (f, args)
   | App (f, args), Proj (p, c) ->
       (match kind f with
-      | Const (p', u) when Constant.equal (Projection.constant p) p' ->
+      | Const (p', u) when Environ.QConstant.equal env (Projection.constant p) p' ->
           let npars = Projection.npars p in
           if Array.length args == npars + 1 then
             eqc' 0 c args.(npars)
diff --git a/engine/termops.ml b/engine/termops.ml
index 467b269e37..3116b03c4f 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1145,7 +1145,7 @@ let compare_constr_univ sigma f cv_pb t1 t2 =
       Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2)
     | Prod (_,t1,c1), Prod (_,t2,c2) ->
         f Reduction.CONV t1 t2 && f cv_pb c1 c2
-    | Const (c, u), Const (c', u') -> Constant.equal c c'
+    | Const (c, u), Const (c', u') -> Constant.CanOrd.equal c c'
     | Ind (i, _), Ind (i', _) -> eq_ind 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/kernel/constr.ml b/kernel/constr.ml
index 1837a39764..fb1e4d12da 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -353,7 +353,7 @@ let isRef c = match kind c with
 let isRefX x c =
   let open GlobRef in
   match x, kind c with
-  | ConstRef c, Const (c', _) -> Constant.equal c c'
+  | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c'
   | IndRef i, Ind (i', _) -> eq_ind i i'
   | ConstructRef i, Construct (i', _) -> eq_constructor i i'
   | VarRef id, Var id' -> Id.equal id id'
@@ -954,7 +954,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2
   | Const (c1,u1), Const (c2,u2) ->
     (* The args length currently isn't used but may as well pass it. *)
-    Constant.equal c1 c2 && leq_universes (Some (GlobRef.ConstRef c1, nargs)) u1 u2
+    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
   | Construct (c1,u1), Construct (c2,u2) ->
     eq_constructor c1 c2 && leq_universes (Some (GlobRef.ConstructRef c1, nargs)) u1 u2
@@ -1442,7 +1442,7 @@ let rec hash t =
     | Evar (e,l) ->
       combinesmall 8 (combine (Evar.hash e) (hash_term_list l))
     | Const (c,u) ->
-      combinesmall 9 (combine (Constant.hash c) (Instance.hash u))
+      combinesmall 9 (combine (Constant.CanOrd.hash c) (Instance.hash u))
     | Ind (ind,u) ->
       combinesmall 10 (combine (ind_hash ind) (Instance.hash u))
     | Construct (c,u) ->
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index b9f434f179..ee90ad382b 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -159,7 +159,7 @@ let hcons_const_body cb =
 let eq_nested_type t1 t2 = match t1, t2 with
 | NestedInd ind1, NestedInd ind2 -> Names.eq_ind ind1 ind2
 | NestedInd _, _ -> false
-| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.equal c1 c2
+| NestedPrimitive c1, NestedPrimitive c2 -> Names.Constant.CanOrd.equal c1 c2
 | NestedPrimitive _, _ -> false
 
 let eq_recarg r1 r2 = match r1, r2 with
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d751d9875a..2b1a295620 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -472,7 +472,7 @@ let inter_recarg r1 r2 = match r1, r2 with
 | Nested (NestedInd i1), Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None
 | Nested (NestedInd _), _ -> None
 | Nested (NestedPrimitive c1), Nested (NestedPrimitive c2) ->
-  if Names.Constant.equal c1 c2 then Some r1 else None
+  if Names.Constant.CanOrd.equal c1 c2 then Some r1 else None
 | Nested (NestedPrimitive _), _ -> None
 
 let inter_wf_paths = Rtree.inter Declareops.eq_recarg inter_recarg Norec
@@ -644,7 +644,7 @@ let abstract_mind_lc ntyps npars lc =
 
 let is_primitive_positive_container env c =
   match env.retroknowledge.Retroknowledge.retro_array with
-  | Some c' when Constant.equal c c' -> true
+  | Some c' when QConstant.equal env c c' -> true
   | _ -> false
 
 (* [get_recargs_approx env tree ind args] builds an approximation of the recargs
@@ -673,7 +673,7 @@ let get_recargs_approx env tree ind args =
        end
     | Const (c,_) when is_primitive_positive_container env c ->
        begin match dest_recarg tree with
-             | Nested (NestedPrimitive c') when Constant.equal c c' ->
+             | Nested (NestedPrimitive c') when QConstant.equal env c c' ->
                build_recargs_nested_primitive ienv tree (c, largs)
              | _ -> mk_norec
        end
diff --git a/kernel/names.ml b/kernel/names.ml
index 592b5e65f7..f987b1d92e 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -529,6 +529,7 @@ module KerPair = struct
   end
 
   module SyntacticOrd = struct
+    type t = kernel_pair
     let compare x y = match x, y with
       | Same knx, Same kny -> KerName.compare knx kny
       | Dual (knux,kncx), Dual (knuy,kncy) ->
diff --git a/kernel/names.mli b/kernel/names.mli
index ea137ad1f4..9a01ea2b43 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -341,27 +341,30 @@ sig
   (** Comparisons *)
 
   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
 
-  val equal : t -> t -> bool
+  val equal : t -> t -> bool [@@ocaml.deprecated "Use QConstant.equal"]
   (** Default comparison, alias for [CanOrd.equal] *)
 
-  val hash : t -> int
+  val hash : t -> int [@@ocaml.deprecated "Use QConstant.hash"]
   (** Hashing function *)
 
   val change_label : t -> Label.t -> t
@@ -431,27 +434,30 @@ sig
   (** Comparisons *)
 
   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
 
-  val equal : t -> t -> bool
-  (** Default comparison, alias for [CanOrd.equal] *)
+  val equal : t -> t -> bool [@@ocaml.deprecated "Use QMutInd.equal"]
+ (** Default comparison, alias for [CanOrd.equal] *)
 
-  val hash : t -> int
+  val hash : t -> int [@@ocaml.deprecated "Use QMutInd.hash"]
 
   (** Displaying *)
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ae070e6f8e..9314203e04 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -67,7 +67,7 @@ let eq_gname gn1 gn2 =
   | Gind (s1, ind1), Gind (s2, ind2) ->
      String.equal s1 s2 && eq_ind ind1 ind2
   | Gconstant (s1, c1), Gconstant (s2, c2) ->
-      String.equal s1 s2 && Constant.equal c1 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
   | Gcase (None, i1), Gcase (None, i2) -> Int.equal i1 i2
@@ -98,7 +98,7 @@ let gname_hash gn = match gn with
 | Gind (s, ind) ->
    combinesmall 1 (combine (String.hash s) (ind_hash ind))
 | Gconstant (s, c) ->
-   combinesmall 2 (combine (String.hash s) (Constant.hash 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))
 | Gpred (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
 | Gfixtype (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
@@ -148,7 +148,7 @@ let eq_symbol sy1 sy2 =
   | SymbValue v1, SymbValue v2 -> (=) v1 v2 (** FIXME: how is this even valid? *)
   | SymbSort s1, SymbSort s2 -> Sorts.equal s1 s2
   | SymbName n1, SymbName n2 -> Name.equal n1 n2
-  | SymbConst kn1, SymbConst kn2 -> Constant.equal kn1 kn2
+  | 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
   | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2
@@ -162,7 +162,7 @@ let hash_symbol symb =
   | SymbValue v -> combinesmall 1 (Hashtbl.hash v) (** FIXME *)
   | SymbSort s -> combinesmall 2 (Sorts.hash s)
   | SymbName name -> combinesmall 3 (Name.hash name)
-  | SymbConst c -> combinesmall 4 (Constant.hash c)
+  | SymbConst c -> combinesmall 4 (Constant.CanOrd.hash c)
   | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw)
   | SymbInd ind -> combinesmall 6 (ind_hash ind)
   | SymbMeta m -> combinesmall 7 m
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index fc6afb79d4..00418009c7 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -83,7 +83,7 @@ and conv_atom env pb lvl a1 a2 cu =
        if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
        else raise NotConvertible
     | Aconstant (c1,u1), Aconstant (c2,u2) ->
-       if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
+       if Constant.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
        else raise NotConvertible
     | Asort s1, Asort s2 ->
         sort_cmp_universes env pb s1 s2 cu
diff --git a/kernel/primred.ml b/kernel/primred.ml
index f158cfacea..17e5a89b74 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -12,7 +12,7 @@ type _ action_kind =
 type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
 
 let check_same_types typ c1 c2 =
-  if not (Constant.equal c1 c2)
+  if not (Constant.CanOrd.equal c1 c2)
   then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
 
 let check_same_inds ind i1 i2 =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 96bf370342..f295b36b60 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -283,7 +283,7 @@ let convert_constructors ctor nargs u1 u2 (s, check) =
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
   match k1, k2 with
-  | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' ->
+  | ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' ->
     if Univ.Instance.equal u u' then cuniv
     else
       let flex = evaluable_constant cst (info_env infos)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 76a1c190be..1a4c786e43 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -182,7 +182,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   begin
     let kn2' = kn_of_delta reso2 kn2 in
     if KerName.equal kn2 kn2' ||
-       MutInd.equal (mind_of_delta_kn reso1 kn1)
+       MutInd.CanOrd.equal (mind_of_delta_kn reso1 kn1)
                     (subst_mind subst2 (MutInd.make kn2 kn2'))
     then ()
     else error NotEqualInductiveAliases
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index ec8601edc9..42908a7363 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -36,7 +36,7 @@ let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_annot _, _ -> false
 | Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2
 | Reloc_const _, _ -> false
-| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2
+| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.CanOrd.equal c1 c2
 | Reloc_getglobal _, _ -> false
 | Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2
 | Reloc_proj_name _, _ -> false
@@ -48,7 +48,7 @@ let hash_reloc_info r =
   match r with
   | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
   | Reloc_const c -> combinesmall 2 (hash_structured_constant c)
-  | Reloc_getglobal c -> combinesmall 3 (Constant.hash c)
+  | Reloc_getglobal c -> combinesmall 3 (Constant.CanOrd.hash c)
   | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p)
   | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p)
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 2068133b10..28a7abc7c6 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -250,7 +250,7 @@ type id_key =
 | EvarKey of Evar.t
 
 let eq_id_key (k1 : id_key) (k2 : id_key) = match k1, k2 with
-| ConstKey c1, ConstKey c2 -> Constant.equal c1 c2
+| ConstKey c1, ConstKey c2 -> Constant.CanOrd.equal c1 c2
 | VarKey id1, VarKey id2 -> Id.equal id1 id2
 | RelKey n1, RelKey n2 -> Int.equal n1 n2
 | EvarKey evk1, EvarKey evk2 -> Evar.equal evk1 evk2
@@ -469,7 +469,7 @@ struct
   let equal = eq_id_key
   open Hashset.Combine
   let hash : t -> tag = function
-  | ConstKey c -> combinesmall 1 (Constant.hash c)
+  | ConstKey c -> combinesmall 1 (Constant.CanOrd.hash c)
   | VarKey id -> combinesmall 2 (Id.hash id)
   | RelKey i -> combinesmall 3 (Int.hash i)
   | EvarKey evk -> combinesmall 4 (Evar.hash evk)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 2dca1d5e49..6869f9c47e 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -741,7 +741,7 @@ and extract_cst_app env sg mle mlt kn args =
   (* Can we instantiate types variables for this constant ? *)
   (* In Ocaml, inside the definition of this constant, the answer is no. *)
   let instantiated =
-    if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints
+    if lang () == Ocaml && List.mem_f Constant.CanOrd.equal kn !current_fixpoints
     then var2var' (snd schema)
     else instantiation schema
   in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index f8449bcda1..e56d66ca2d 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -32,7 +32,7 @@ module Refset' = GlobRef.Set_env
 
 let occur_kn_in_ref kn = let open GlobRef in function
   | IndRef (kn',_)
-  | ConstructRef ((kn',_),_) -> MutInd.equal kn kn'
+  | ConstructRef ((kn',_),_) -> MutInd.CanOrd.equal kn kn'
   | ConstRef _ | VarRef _ -> false
 
 let repr_of_r = let open GlobRef in function
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index e50c6087bb..73eb943418 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -674,7 +674,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
            |Prod _ ->
             let new_infos = {dyn_infos with info = (f, args)} in
             build_proof_args env sigma do_finalize new_infos
-          | Const (c, _) when not (List.mem_f Constant.equal c fnames) ->
+          | Const (c, _) when not (List.mem_f Constant.CanOrd.equal c fnames) ->
             let new_infos = {dyn_infos with info = (f, args)} in
             (*                    Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *)
             build_proof_args env sigma do_finalize new_infos
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1ab747ca09..0ab9ac65d7 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -100,8 +100,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
   let is_dom c =
     match Constr.kind c with
-    | Ind ((u, _), _) -> MutInd.equal u rel_as_kn
-    | Construct (((u, _), _), _) -> MutInd.equal u rel_as_kn
+    | Ind ((u, _), _) -> Environ.QMutInd.equal env u rel_as_kn
+    | Construct (((u, _), _), _) -> Environ.QMutInd.equal env u rel_as_kn
     | _ -> false
   in
   let get_fun_num c =
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 012fcee486..314c8abcaf 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1316,9 +1316,9 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list =
   let prop_sort = Sorts.InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
+    let eq c1 c2 = Environ.QConstant.equal env c1 c2 in
     List.map
-      (function
-        | cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes)
+      (function cst -> List.assoc_f eq (fst cst) this_block_funs_indexes)
       funs
   in
   let ind_list =
@@ -2228,7 +2228,8 @@ let build_case_scheme fa =
   let prop_sort = Sorts.InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
-    List.assoc_f Constant.equal funs this_block_funs_indexes
+    let eq c1 c2 = Environ.QConstant.equal env c1 c2 in
+    List.assoc_f eq funs this_block_funs_indexes
   in
   let ind, sf =
     let ind = (first_fun_kn, funs_indexes) in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 5d631aac84..118a917381 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -27,12 +27,13 @@ open Indfun_common
 *)
 let revert_graph kn post_tac hid =
   Proofview.Goal.enter (fun gl ->
+      let env = Proofview.Goal.env gl in
       let sigma = project gl in
       let typ = pf_get_hyp_typ hid gl in
       match EConstr.kind sigma typ with
       | App (i, args) when isInd sigma i ->
         let ((kn', num) as ind'), u = destInd sigma i in
-        if MutInd.equal kn kn' then
+        if Environ.QMutInd.equal env kn kn' then
           (* We have generated a graph hypothesis so that we must change it if we can *)
           let info =
             match find_Function_of_graph ind' with
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 5ef76dbdc1..3e4a96b10d 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -968,7 +968,7 @@ let fold_match ?(force=false) env sigma c =
 
 let unfold_match env sigma sk app =
   match EConstr.kind sigma app with
-  | App (f', args) when Constant.equal (fst (destConst sigma f')) sk ->
+  | App (f', args) when QConstant.equal env (fst (destConst sigma f')) sk ->
       let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
       let v = EConstr.of_constr v in
         Reductionops.whd_beta env sigma (mkApp (v, args))
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index cdd15acb0d..bd514f15d5 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -463,8 +463,8 @@ let nb_cs_proj_args pc f u =
   try match kind f with
   | Prod _ -> na Prod_cs
   | Sort s -> na (Sort_cs (Sorts.family s))
-  | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f
-  | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f
+  | Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f
+  | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f
   | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f))
   | _ -> -1
   with Not_found -> -1
@@ -508,7 +508,7 @@ let filter_upat i0 f n u fpats =
   let () = if !i0 < np then i0 := n in (u, np) :: fpats
 
 let eq_prim_proj c t = match kind t with
-  | Proj(p,_) -> Constant.equal (Projection.constant p) c
+  | Proj(p,_) -> Constant.CanOrd.equal (Projection.constant p) c
   | _ -> false
 
 let filter_upat_FO i0 f n u fpats =
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 419eeaa92a..71ef166ff0 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -244,7 +244,7 @@ let matches_core env sigma allow_bound_rels
     let open GlobRef in
     match ref, EConstr.kind sigma c with
     | VarRef id, Var id' -> Names.Id.equal id id'
-    | ConstRef c, Const (c',_) -> Constant.equal c c'
+    | ConstRef c, Const (c',_) -> Environ.QConstant.equal env c c'
     | IndRef i, Ind (i', _) -> Names.eq_ind i i'
     | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
     | _, _ -> false
@@ -307,7 +307,7 @@ let matches_core env sigma allow_bound_rels
 
       | PApp (c1,arg1), App (c2,arg2) ->
         (match c1, EConstr.kind sigma c2 with
-        | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr))
+        | PRef (GlobRef.ConstRef r), Proj (pr,c) when not (Environ.QConstant.equal env r (Projection.constant pr))
             || Projection.unfolded pr ->
           raise PatternMatchingFailure
         | PProj (pr1,c1), Proj (pr,c) ->
@@ -324,7 +324,7 @@ let matches_core env sigma allow_bound_rels
           with Invalid_argument _ -> raise PatternMatchingFailure)
 
       | PApp (PRef (GlobRef.ConstRef c1), _), Proj (pr, c2)
-        when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) ->
+        when Projection.unfolded pr || not (Environ.QConstant.equal env c1 (Projection.constant pr)) ->
         raise PatternMatchingFailure
 
       | PApp (c, args), Proj (pr, c2) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a5311e162d..6a668e79e8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -566,7 +566,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     in
     let compare_heads evd =
       match EConstr.kind evd term, EConstr.kind evd term' with
-      | Const (c, u), Const (c', u') when Constant.equal c c' ->
+      | Const (c, u), Const (c', u') when QConstant.equal env c c' ->
         let u = EInstance.kind evd u and u' = EInstance.kind evd u' in
         check_strict evd u u'
       | Const _, Const _ -> UnifFailure (evd, NotSameHead)
@@ -844,7 +844,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
             ise_try evd [f1; f2]
 
         (* Catch the p.c ~= p c' cases *)
-        | Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' ->
+        | Proj (p,c), Const (p',u) when QConstant.equal env (Projection.constant p) p' ->
           let res =
             try Some (destApp evd (Retyping.expand_projection env evd p c []))
             with Retyping.RetypeError _ -> None
@@ -855,7 +855,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
                 appr2
             | None -> UnifFailure (evd,NotSameHead))
 
-        | Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') ->
+        | Const (p,u), Proj (p',c') when QConstant.equal env p (Projection.constant p') ->
           let res =
             try Some (destApp evd (Retyping.expand_projection env evd p' c' []))
             with Retyping.RetypeError _ -> None
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index eaf8c65811..13abf47413 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -206,7 +206,7 @@ let is_array_const env sigma c =
   | Const (cst,_) ->
     (match env.Environ.retroknowledge.Retroknowledge.retro_array with
      | None -> false
-     | Some cst' -> Constant.equal cst cst')
+     | Some cst' -> Environ.QConstant.equal env cst cst')
   | _ -> false
 
 let split_as_array env sigma0 = function
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 5be8f9f83c..5ffd919312 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -584,7 +584,7 @@ let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function
         (List.map
            (function ((mind',u'),dep',s') ->
               let (sp',_) = mind' in
-              if MutInd.equal sp sp' then
+              if QMutInd.equal env sp sp' then
                 let (mibi',mipi') = lookup_mind_specif env mind' in
                 ((mind',u'),mibi',mipi',dep',s')
               else
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9d15e98373..d94cae75bd 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -82,7 +82,7 @@ type evaluable_reference =
   | EvalEvar of EConstr.existential
 
 let evaluable_reference_eq sigma r1 r2 = match r1, r2 with
-| EvalConst c1, EvalConst c2 -> Constant.equal c1 c2
+| EvalConst c1, EvalConst c2 -> Constant.CanOrd.equal c1 c2
 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2
 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2
 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
@@ -995,7 +995,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
       | CoFix _ | Fix _ -> s'
       | Proj (p,t) when
           (match EConstr.kind sigma constr with
-          | Const (c', _) -> Constant.equal (Projection.constant p) c'
+          | Const (c', _) -> Constant.CanOrd.equal (Projection.constant p) c'
           | _ -> false) ->
         let npars = Projection.npars p in
           if List.length stack <= npars then
@@ -1101,7 +1101,7 @@ let contextually byhead occs f env sigma t =
 
 let match_constr_evaluable_ref sigma c evref =
   match EConstr.kind sigma c, evref with
-  | Const (c,u), EvalConstRef c' when Constant.equal c c' -> Some u
+  | Const (c,u), EvalConstRef c' when Constant.CanOrd.equal c c' -> Some u
   | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty
   | _, _ -> None
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ccfb508964..08303c80d6 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -547,10 +547,10 @@ let oracle_order env cf1 cf2 =
       | Some k2 ->
         match k1, k2 with
         | IsProj (p, _), IsKey (ConstKey (p',_))
-          when Constant.equal (Projection.constant p) p' ->
+          when Environ.QConstant.equal env (Projection.constant p) p' ->
           Some (not (Projection.unfolded p))
         | IsKey (ConstKey (p,_)), IsProj (p', _)
-          when Constant.equal p (Projection.constant p') ->
+          when Environ.QConstant.equal env p (Projection.constant p') ->
           Some (Projection.unfolded p')
         | _ ->
           Some (Conv_oracle.oracle_order (fun x -> x)
@@ -796,7 +796,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
         | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c)
 
         (* Fast path for projections. *)
-        | Proj (p1,c1), Proj (p2,c2) when Constant.equal
+        | Proj (p1,c1), Proj (p2,c2) when Environ.QConstant.equal env
             (Projection.constant p1) (Projection.constant p2) ->
           (try unify_same_proj curenvnb cv_pb {opt with at_top = true}
                substn c1 c2
@@ -914,7 +914,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
         match EConstr.kind sigma c' with
         | Meta _ -> true
         | Evar _ -> true
-        | Const (c, u) -> Constant.equal c (Projection.constant p)
+        | Const (c, u) -> Environ.QConstant.equal env c (Projection.constant p)
         | _ -> false
       in
       let expand_proj c c' l =
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 0b13f4763a..bec9ede6f1 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -225,7 +225,7 @@ struct
     let equal_cst_member x y =
       match x, y with
       | Cst_const (c1,u1), Cst_const (c2, u2) ->
-        Constant.equal c1 c2 && Univ.Instance.equal u1 u2
+        Constant.CanOrd.equal c1 c2 && Univ.Instance.equal u1 u2
       | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2
       | _, _ -> false
     in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a607c09010..f3ecc2a9f0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -540,7 +540,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
   | (f, n, ar) :: oth ->
     let open Context.Named.Declaration in
     let (sp', u')  = check_mutind env sigma n ar in
-    if not (MutInd.equal sp sp') then
+    if not (QMutInd.equal env sp sp') then
       error "Fixpoints should be on the same mutual inductive declaration.";
     if mem_named_context_val f sign then
       user_err ~hdr:"Logic.prim_refiner"
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 7a7e7d6e35..475d4e9af9 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -145,7 +145,7 @@ let build_beq_scheme_deps kn =
       | Cast (x,_,_) -> aux accu (Term.applist (x,a))
       | App _ -> assert false
       | Ind ((kn', _), _) ->
-          if MutInd.equal kn kn' then accu
+          if Environ.QMutInd.equal env kn kn' then accu
           else
             let eff = SchemeMutualDep (kn', !beq_scheme_kind_aux ()) in
             List.fold_left aux (eff :: accu) a
@@ -253,7 +253,7 @@ let build_beq_scheme mode kn =
         | Cast (x,_,_) -> aux (Term.applist (x,a))
         | App _ -> assert false
         | Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
-            if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
+            if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
             else begin
               try
                 let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with
@@ -539,7 +539,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
         with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
       end
   end >>= fun (sp2,i2) ->
-  if not (MutInd.equal sp1 sp2) || not (Int.equal i1 i2)
+  Proofview.tclENV >>= fun env ->
+  if not (Environ.QMutInd.equal env sp1 sp2) || not (Int.equal i1 i2)
   then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
   else aux (Array.to_list ca1) (Array.to_list ca2)
 
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 5274a6da3b..7d0c5ee48f 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -162,7 +162,7 @@ let cache_constant ((sp,kn), obj) =
     then Constant.make1 kn
     else CErrors.anomaly Pp.(str"Missing constant " ++ Id.print(Libnames.basename sp) ++ str".")
   in
-  assert (Constant.equal kn' (Constant.make1 kn));
+  assert (Environ.QConstant.equal (Global.env ()) kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (GlobRef.ConstRef (Constant.make1 kn));
   Dumpglob.add_constant_kind (Constant.make1 kn) obj.cst_kind
 
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 356ccef06b..de72a30f18 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -405,7 +405,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
 let get_common_underlying_mutual_inductive env = function
   | [] -> assert false
   | (id,(mind,i as ind))::l as all ->
-      match List.filter (fun (_,(mind',_)) -> not (MutInd.equal mind mind')) l with
+      match List.filter (fun (_,(mind',_)) -> not (Environ.QMutInd.equal env mind mind')) l with
       | (_,ind')::_ ->
           raise (RecursionSchemeError (env, NotMutualInScheme (ind,ind')))
       | [] ->
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml
index 534c358a3f..79468627de 100644
--- a/vernac/recLemmas.ml
+++ b/vernac/recLemmas.ml
@@ -44,7 +44,7 @@ let find_mutually_recursive_statements sigma thms =
             [] in
       ind_hyps,ind_ccl) thms in
     let inds_hyps,ind_ccls = List.split inds in
-    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Names.MutInd.equal kn kn' in
+    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> Environ.QMutInd.equal (Global.env ()) kn kn' in
     (* Check if all conclusions are coinductive in the same type *)
     (* (degenerated cartesian product since there is at most one coind ccl) *)
     let same_indccl =
-- 
cgit v1.2.3


From 0590764209dcb8540b5292aca38fe2df38b90ab9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Sep 2020 14:19:20 +0200
Subject: Same little game with Projection.

---
 kernel/names.ml       |  8 ++++++++
 kernel/names.mli      | 11 ++++++++---
 kernel/reduction.ml   |  4 ++--
 kernel/vconv.ml       |  2 +-
 kernel/vmemitcodes.ml |  4 ++--
 kernel/vmsymtable.ml  |  2 +-
 pretyping/evarconv.ml |  4 ++--
 tactics/cbn.ml        |  2 +-
 8 files changed, 25 insertions(+), 12 deletions(-)

diff --git a/kernel/names.ml b/kernel/names.ml
index f987b1d92e..5f2ecea5f0 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -787,6 +787,8 @@ struct
       Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind)
 
     module SyntacticOrd = struct
+      type nonrec t = t
+
       let compare a b =
         let c = ind_syntactic_ord a.proj_ind b.proj_ind in
         if c == 0 then Int.compare a.proj_arg b.proj_arg
@@ -799,6 +801,8 @@ struct
         Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind)
     end
     module CanOrd = struct
+      type nonrec t = t
+
       let compare a b =
         let c = ind_ord a.proj_ind b.proj_ind in
         if c == 0 then Int.compare a.proj_arg b.proj_arg
@@ -811,6 +815,8 @@ struct
         Hashset.Combine.combinesmall p.proj_arg (ind_hash p.proj_ind)
     end
     module UserOrd = struct
+      type nonrec t = t
+
       let compare a b =
         let c = ind_user_ord a.proj_ind b.proj_ind in
         if c == 0 then Int.compare a.proj_arg b.proj_arg
@@ -877,6 +883,7 @@ struct
   let hash (c, b) = (if b then 0 else 1) + Repr.hash c
 
   module SyntacticOrd = struct
+    type nonrec t = t
     let compare (c, b) (c', b') =
       if b = b' then Repr.SyntacticOrd.compare c c' else -1
     let equal (c, b as x) (c', b' as x') =
@@ -884,6 +891,7 @@ struct
     let hash (c, b) = (if b then 0 else 1) + Repr.SyntacticOrd.hash c
   end
   module CanOrd = struct
+    type nonrec t = t
     let compare (c, b) (c', b') =
       if b = b' then Repr.CanOrd.compare c c' else -1
     let equal (c, b as x) (c', b' as x') =
diff --git a/kernel/names.mli b/kernel/names.mli
index 9a01ea2b43..a0320fda43 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -565,16 +565,19 @@ module Projection : sig
     val make : inductive -> proj_npars:int -> proj_arg:int -> Label.t -> t
 
     module SyntacticOrd : sig
+      type nonrec t = t
       val compare : t -> t -> int
       val equal : t -> t -> bool
       val hash : t -> int
     end
     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
@@ -589,9 +592,9 @@ module Projection : sig
     val arg : t -> int
     val label : t -> Label.t
 
-    val equal : t -> t -> bool
-    val hash : t -> int
-    val compare : t -> t -> int
+    val equal : t -> t -> bool [@@ocaml.deprecated "Use QProjection.equal"]
+    val hash : t -> int [@@ocaml.deprecated "Use QProjection.hash"]
+    val compare : t -> t -> int [@@ocaml.deprecated "Use QProjection.compare"]
 
     val map : (MutInd.t -> MutInd.t) -> t -> t
     val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t
@@ -609,11 +612,13 @@ module Projection : sig
   val repr : t -> Repr.t
 
   module SyntacticOrd : sig
+    type nonrec t = t
     val compare : t -> t -> int
     val equal : t -> t -> bool
     val hash : t -> int
   end
   module CanOrd : sig
+    type nonrec t = t
     val compare : t -> t -> int
     val equal : t -> t -> bool
     val hash : t -> int
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f295b36b60..8eb1c10f70 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -441,7 +441,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         | Some s2 ->
           eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
         | None ->
-          if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
+          if Projection.Repr.CanOrd.equal (Projection.repr p1) (Projection.repr p2)
              && compare_stack_shape v1 v2 then
             let el1 = el_stack lft1 v1 in
             let el2 = el_stack lft2 v2 in
@@ -704,7 +704,7 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
             | (Zlapp a1,Zlapp a2) ->
                Array.fold_right2 f a1 a2 cu1
             | (Zlproj (c1,_l1),Zlproj (c2,_l2)) ->
-              if not (Projection.Repr.equal c1 c2) then
+              if not (Projection.Repr.CanOrd.equal c1 c2) then
                 raise NotConvertible
               else cu1
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 948195797e..2de902c827 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -141,7 +141,7 @@ and conv_stack env k stk1 stk2 cu =
         conv_stack env k stk1 stk2 !rcu
       else raise NotConvertible
   | Zproj p1 :: stk1, Zproj p2 :: stk2 ->
-    if Projection.Repr.equal p1 p2 then conv_stack env k stk1 stk2 cu
+    if Projection.Repr.CanOrd.equal p1 p2 then conv_stack env k stk1 stk2 cu
     else raise NotConvertible
   | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
   | Zproj _ :: _, _ -> raise NotConvertible
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index 42908a7363..babc57794b 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -38,7 +38,7 @@ let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_const _, _ -> false
 | Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.CanOrd.equal c1 c2
 | Reloc_getglobal _, _ -> false
-| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2
+| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.CanOrd.equal p1 p2
 | Reloc_proj_name _, _ -> false
 | Reloc_caml_prim p1, Reloc_caml_prim p2 -> CPrimitives.equal p1 p2
 | Reloc_caml_prim _, _ -> false
@@ -49,7 +49,7 @@ let hash_reloc_info r =
   | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
   | Reloc_const c -> combinesmall 2 (hash_structured_constant c)
   | Reloc_getglobal c -> combinesmall 3 (Constant.CanOrd.hash c)
-  | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p)
+  | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.CanOrd.hash p)
   | Reloc_caml_prim p -> combinesmall 5 (CPrimitives.hash p)
 
 module RelocTable = Hashtbl.Make(struct
diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml
index 9d80dc578b..ae0fa38571 100644
--- a/kernel/vmsymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -85,7 +85,7 @@ module AnnotTable = Hashtbl.Make (struct
   let hash = hash_annot_switch
 end)
 
-module ProjNameTable = Hashtbl.Make (Projection.Repr)
+module ProjNameTable = Hashtbl.Make (Projection.Repr.CanOrd)
 
 let str_cst_tbl : int SConstTable.t = SConstTable.create 31
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6a668e79e8..08cb173442 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -387,7 +387,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
         | UnifFailure _ as x -> fail x)
       | UnifFailure _ as x -> fail x)
     | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 ->
-       if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
+       if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2)
        then ise_stack2 true i q1 q2
        else fail (UnifFailure (i, NotSameHead))
     | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1,
@@ -429,7 +429,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
           (fun i -> ise_stack2 i a1 a2)]
       else UnifFailure (i,NotSameHead)
     | Stack.Proj (p1)::q1, Stack.Proj (p2)::q2 ->
-       if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2)
+       if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2)
        then ise_stack2 i q1 q2
        else (UnifFailure (i, NotSameHead))
     | Stack.App _ :: _, Stack.App _ :: _ ->
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index bec9ede6f1..5838bbcc19 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -239,7 +239,7 @@ struct
       | Case (_,t1,_,a1,_) :: s1, Case (_,t2,_,a2,_) :: s2 ->
         f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
       | (Proj (p,_)::s1, Proj(p2,_)::s2) ->
-        Projection.Repr.equal (Projection.repr p) (Projection.repr p2)
+        Projection.Repr.CanOrd.equal (Projection.repr p) (Projection.repr p2)
         && equal_rec s1 s2
       | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' ->
         f_fix f1 f2
-- 
cgit v1.2.3


From 0a46af10ffc38726207bca952775102d48ad3b15 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Sep 2020 18:36:10 +0200
Subject: Rename the GlobRef comparison modules following the standard pattern.

---
 interp/notation.ml              | 2 +-
 interp/reserve.ml               | 2 +-
 kernel/names.ml                 | 8 ++++----
 kernel/names.mli                | 4 ++--
 library/coqlib.ml               | 2 +-
 library/globnames.ml            | 6 +++---
 plugins/firstorder/instances.ml | 2 +-
 plugins/firstorder/sequent.ml   | 2 +-
 pretyping/keys.ml               | 6 +++---
 printing/printer.ml             | 2 +-
 tactics/btermdn.ml              | 2 +-
 tactics/term_dnet.ml            | 2 +-
 12 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/interp/notation.ml b/interp/notation.ml
index d57c4f3abf..269e20c16e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -323,7 +323,7 @@ type key =
   | Oth
 
 let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.CanOrd.compare gr1 gr2
 | RefKey _, Oth -> -1
 | Oth, RefKey _ -> 1
 | Oth, Oth -> 0
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 4418a32645..1d5af3ff39 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -28,7 +28,7 @@ type key =
 (** TODO: share code from Notation *)
 
 let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.CanOrd.compare gr1 gr2
 | RefKey _, Oth -> -1
 | Oth, RefKey _ -> 1
 | Oth, Oth -> 0
diff --git a/kernel/names.ml b/kernel/names.ml
index 5f2ecea5f0..f7658df355 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -991,7 +991,7 @@ module GlobRef = struct
 
   (* By default, [global_reference] are ordered on their canonical part *)
 
-  module Ordered = struct
+  module CanOrd = struct
     open Constant.CanOrd
     type t = GlobRefInternal.t
     let compare gr1 gr2 =
@@ -1000,7 +1000,7 @@ module GlobRef = struct
     let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr
   end
 
-  module Ordered_env = struct
+  module UserOrd = struct
     open Constant.UserOrd
     type t = GlobRefInternal.t
     let compare gr1 gr2 =
@@ -1010,12 +1010,12 @@ module GlobRef = struct
     let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr
   end
 
-  module Map = HMap.Make(Ordered)
+  module Map = HMap.Make(CanOrd)
   module Set = Map.Set
 
   (* Alternative sets and maps indexed by the user part of the kernel names *)
 
-  module Map_env = HMap.Make(Ordered_env)
+  module Map_env = HMap.Make(UserOrd)
   module Set_env = Map_env.Set
 
 end
diff --git a/kernel/names.mli b/kernel/names.mli
index a0320fda43..76be6ca105 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -667,14 +667,14 @@ module GlobRef : sig
 
   val equal : t -> t -> bool
 
-  module Ordered : sig
+  module CanOrd : sig
     type nonrec t = t
     val compare : t -> t -> int
     val equal : t -> t -> bool
     val hash : t -> int
   end
 
-  module Ordered_env : sig
+  module UserOrd : sig
     type nonrec t = t
     val compare : t -> t -> int
     val equal : t -> t -> bool
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 04a6e159eb..b374ecbca0 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -84,7 +84,7 @@ let gen_reference_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let qualid = qualid_of_string s in
   let all = Nametab.locate_all qualid in
-  let all = List.sort_uniquize GlobRef.Ordered_env.compare all in
+  let all = List.sort_uniquize GlobRef.UserOrd.compare all in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
     | [x] -> x
diff --git a/library/globnames.ml b/library/globnames.ml
index bc24fbf096..654349dea0 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -98,14 +98,14 @@ module ExtRefOrdered = struct
   let equal x y =
     x == y ||
     match x, y with
-    | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry
+    | TrueGlobal rx, TrueGlobal ry -> GlobRef.UserOrd.equal rx ry
     | SynDef knx, SynDef kny -> KerName.equal knx kny
     | (TrueGlobal _ | SynDef _), _ -> false
 
   let compare x y =
     if x == y then 0
     else match x, y with
-      | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry
+      | TrueGlobal rx, TrueGlobal ry -> GlobRef.UserOrd.compare rx ry
       | SynDef knx, SynDef kny -> KerName.compare knx kny
       | TrueGlobal _, SynDef _ -> -1
       | SynDef _, TrueGlobal _ -> 1
@@ -113,7 +113,7 @@ module ExtRefOrdered = struct
   open Hashset.Combine
 
   let hash = function
-  | TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr)
+  | TrueGlobal gr -> combinesmall 1 (GlobRef.UserOrd.hash gr)
   | SynDef kn -> combinesmall 2 (KerName.hash kn)
 
 end
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index f13901c36d..4adad53899 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -38,7 +38,7 @@ let compare_gr id1 id2 =
   if id1==id2 then 0 else
     if id1==dummy_id then 1
     else if id2==dummy_id then -1
-    else GlobRef.Ordered.compare id1 id2
+    else GlobRef.CanOrd.compare id1 id2
 
 module OrderedInstance=
 struct
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index db3631daa4..99c5f85125 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -62,7 +62,7 @@ module Hitem=
 struct
   type t = h_item
   let compare (id1,co1) (id2,co2)=
-    let c = GlobRef.Ordered.compare id1 id2 in
+    let c = GlobRef.CanOrd.compare id1 id2 in
     if c = 0 then
       let cmp (i1, c1) (i2, c2) =
         let c = Int.compare i1 i2 in
diff --git a/pretyping/keys.ml b/pretyping/keys.ml
index 7a7099c195..dd3488c1df 100644
--- a/pretyping/keys.ml
+++ b/pretyping/keys.ml
@@ -34,7 +34,7 @@ module KeyOrdered = struct
 
   let hash gr =
     match gr with
-    | KGlob gr -> 9 + GlobRef.Ordered.hash gr
+    | KGlob gr -> 9 + GlobRef.CanOrd.hash gr
     | KLam -> 0
     | KLet -> 1
     | KProd -> 2
@@ -49,14 +49,14 @@ module KeyOrdered = struct
 
   let compare gr1 gr2 =
     match gr1, gr2 with
-    | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2
+    | KGlob gr1, KGlob gr2 -> GlobRef.CanOrd.compare gr1 gr2
     | _, KGlob _ -> -1
     | KGlob _, _ -> 1
     | k, k' -> Int.compare (hash k) (hash k')
 
   let equal k1 k2 =
     match k1, k2 with
-    | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2
+    | KGlob gr1, KGlob gr2 -> GlobRef.CanOrd.equal gr1 gr2
     | _, KGlob _ -> false
     | KGlob _, _ -> false
     | k, k' -> k == k'
diff --git a/printing/printer.ml b/printing/printer.ml
index bc26caefbe..be1cc0d64a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -884,7 +884,7 @@ struct
       MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2
     | TypeInType k1, TypeInType k2 ->
-      GlobRef.Ordered.compare k1 k2
+      GlobRef.CanOrd.compare k1 k2
     | Constant _, _ -> -1
     | _, Constant _ -> 1
     | Positive _, _ -> -1
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index f721e9956b..af0ca22868 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -27,7 +27,7 @@ type term_label =
 | SortLabel
 
 let compare_term_label t1 t2 = match t1, t2 with
-| GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2
+| GRLabel gr1, GRLabel gr2 -> GlobRef.CanOrd.compare gr1 gr2
 | _ -> pervasives_compare t1 t2 (** OK *)
 
 type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 3bcd235b41..fee9dd1b96 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -107,7 +107,7 @@ struct
   | DRel, _ -> -1 | _, DRel -> 1
   | DSort, DSort -> 0
   | DSort, _ -> -1 | _, DSort -> 1
-  | DRef gr1, DRef gr2 -> GlobRef.Ordered.compare gr1 gr2
+  | DRef gr1, DRef gr2 -> GlobRef.CanOrd.compare gr1 gr2
   | DRef _, _ -> -1 | _, DRef _ -> 1
 
   | DCtx (tl1, tr1), DCtx (tl2, tr2)
-- 
cgit v1.2.3


From bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 12:42:21 +0200
Subject: 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.
---
 engine/eConstr.ml             |   2 +-
 engine/termops.ml             |   2 +-
 interp/notation_ops.ml        |   6 +--
 kernel/constr.ml              |  12 ++---
 kernel/cooking.ml             |   4 +-
 kernel/declareops.ml          |   4 +-
 kernel/inductive.ml           |  10 ++--
 kernel/names.ml               | 106 ++++++++++++++++++++++++++----------------
 kernel/names.mli              |  49 +++++++++++++++++--
 kernel/nativecode.ml          |  28 +++++------
 kernel/nativeconv.ml          |   6 +--
 kernel/nativevalues.ml        |   4 +-
 kernel/primred.ml             |   2 +-
 kernel/reduction.ml           |   8 ++--
 kernel/typeops.ml             |   2 +-
 kernel/vconv.ml               |   2 +-
 kernel/vmvalues.ml            |   4 +-
 library/coqlib.ml             |   2 +-
 library/lib.ml                |   2 +-
 plugins/btauto/refl_btauto.ml |   2 +-
 plugins/extraction/mlutil.ml  |   2 +-
 plugins/rtauto/refl_tauto.ml  |   6 +--
 pretyping/cases.ml            |   6 +--
 pretyping/coercion.ml         |  10 ++--
 pretyping/coercionops.ml      |   2 +-
 pretyping/constr_matching.ml  |   4 +-
 pretyping/evarconv.ml         |   2 +-
 pretyping/glob_ops.ml         |   2 +-
 pretyping/patternops.ml       |   4 +-
 pretyping/pretyping.ml        |   2 +-
 pretyping/tacred.ml           |   2 +-
 pretyping/unification.ml      |   2 +-
 tactics/elim.ml               |   2 +-
 tactics/term_dnet.ml          |   2 +-
 vernac/auto_ind_decl.ml       |   2 +-
 vernac/himsg.ml               |   4 +-
 vernac/recLemmas.ml           |   2 +-
 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
-- 
cgit v1.2.3


From aa3d78fefde6897a50273c83f944b6617963a9bc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 13:58:13 +0200
Subject: Similar introduction of a Construct module in the Names API.

---
 engine/eConstr.ml                       |   2 +-
 engine/termops.ml                       |   2 +-
 interp/notation_ops.ml                  |  10 ++--
 kernel/constr.ml                        |  10 ++--
 kernel/cooking.ml                       |   4 +-
 kernel/names.ml                         | 103 +++++++++++++++++++-------------
 kernel/names.mli                        |  47 +++++++++++++--
 kernel/nativelambda.ml                  |   4 +-
 library/lib.ml                          |   2 +-
 plugins/cc/ccalgo.ml                    |   4 +-
 plugins/funind/glob_term_to_relation.ml |   5 +-
 plugins/funind/glob_termops.ml          |   6 +-
 pretyping/constr_matching.ml            |   2 +-
 pretyping/evarconv.ml                   |   2 +-
 pretyping/glob_ops.ml                   |   2 +-
 tactics/equality.ml                     |   2 +-
 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
-- 
cgit v1.2.3


From b71a363519b689612cec74914d10518f102ba869 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 14:19:03 +0200
Subject: Code factorization in Names.

We introduce a module type not to have to redeclare CanOrd, UserOrd and
SyntacticOrd all over the place.
---
 kernel/names.ml  |  47 ++++++++++++++----
 kernel/names.mli | 148 ++++++++++---------------------------------------------
 2 files changed, 63 insertions(+), 132 deletions(-)

diff --git a/kernel/names.ml b/kernel/names.ml
index 65c602b863..5b6064fa9f 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -447,6 +447,22 @@ module KNset = KNmap.Set
 
 (** {6 Kernel pairs } *)
 
+module type EqType =
+sig
+  type t
+  val compare : t -> t -> int
+  val equal : t -> t -> bool
+  val hash : t -> int
+end
+
+module type QNameS =
+sig
+  type t
+  module CanOrd : EqType with type t = t
+  module UserOrd : EqType with type t = t
+  module SyntacticOrd : EqType with type t = t
+end
+
 (** For constant and inductive names, we use a kernel name couple (kn1,kn2)
    where kn1 corresponds to the name used at toplevel (i.e. what the user see)
    and kn2 corresponds to the canonical kernel name i.e. in the environment
@@ -945,6 +961,14 @@ struct
       x == x' || b = b' && Repr.CanOrd.equal c c'
     let hash (c, b) = (if b then 0 else 1) + Repr.CanOrd.hash c
   end
+  module UserOrd = struct
+    type nonrec t = t
+    let compare (c, b) (c', b') =
+      if b = b' then Repr.UserOrd.compare c c' else -1
+    let equal (c, b as x) (c', b' as x') =
+      x == x' || b = b' && Repr.UserOrd.equal c c'
+    let hash (c, b) = (if b then 0 else 1) + Repr.UserOrd.hash c
+  end
 
   module Self_Hashcons =
     struct
@@ -1039,22 +1063,27 @@ module GlobRef = struct
   (* By default, [global_reference] are ordered on their canonical part *)
 
   module CanOrd = struct
-    open Constant.CanOrd
     type t = GlobRefInternal.t
     let compare gr1 gr2 =
-      GlobRefInternal.global_ord_gen compare ind_ord constructor_ord gr1 gr2
-    let equal gr1 gr2 = GlobRefInternal.global_eq_gen equal eq_ind eq_constructor gr1 gr2
-    let hash gr = GlobRefInternal.global_hash_gen hash ind_hash constructor_hash gr
+      GlobRefInternal.global_ord_gen Constant.CanOrd.compare Ind.CanOrd.compare Construct.CanOrd.compare gr1 gr2
+    let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.CanOrd.equal Ind.CanOrd.equal Construct.CanOrd.equal gr1 gr2
+    let hash gr = GlobRefInternal.global_hash_gen Constant.CanOrd.hash Ind.CanOrd.hash Construct.CanOrd.hash gr
   end
 
   module UserOrd = struct
-    open Constant.UserOrd
     type t = GlobRefInternal.t
     let compare gr1 gr2 =
-      GlobRefInternal.global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2
-    let equal gr1 gr2 =
-      GlobRefInternal.global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2
-    let hash gr = GlobRefInternal.global_hash_gen hash ind_user_hash constructor_user_hash gr
+      GlobRefInternal.global_ord_gen Constant.UserOrd.compare Ind.UserOrd.compare Construct.UserOrd.compare gr1 gr2
+    let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.UserOrd.equal Ind.UserOrd.equal Construct.UserOrd.equal gr1 gr2
+    let hash gr = GlobRefInternal.global_hash_gen Constant.UserOrd.hash Ind.UserOrd.hash Construct.UserOrd.hash gr
+  end
+
+  module SyntacticOrd = struct
+    type t = GlobRefInternal.t
+    let compare gr1 gr2 =
+      GlobRefInternal.global_ord_gen Constant.SyntacticOrd.compare Ind.SyntacticOrd.compare Construct.SyntacticOrd.compare gr1 gr2
+    let equal gr1 gr2 = GlobRefInternal.global_eq_gen Constant.SyntacticOrd.equal Ind.SyntacticOrd.equal Construct.SyntacticOrd.equal gr1 gr2
+    let hash gr = GlobRefInternal.global_hash_gen Constant.SyntacticOrd.hash Ind.SyntacticOrd.hash Construct.SyntacticOrd.hash gr
   end
 
   module Map = HMap.Make(CanOrd)
diff --git a/kernel/names.mli b/kernel/names.mli
index 1ba928a416..df4ddab3c2 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -307,6 +307,24 @@ module KNset  : CSig.SetS with type elt = KerName.t
 module KNpred : Predicate.S with type elt = KerName.t
 module KNmap  : Map.ExtS with type key = KerName.t and module Set := KNset
 
+(** {6 Signature for quotiented names} *)
+
+module type EqType =
+sig
+  type t
+  val compare : t -> t -> int
+  val equal : t -> t -> bool
+  val hash : t -> int
+end
+
+module type QNameS =
+sig
+  type t
+  module CanOrd : EqType with type t = t
+  module UserOrd : EqType with type t = t
+  module SyntacticOrd : EqType with type t = t
+end
+
 (** {6 Constant Names } *)
 
 module Constant:
@@ -340,26 +358,7 @@ sig
 
   (** Comparisons *)
 
-  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
+  include QNameS with type t := t
 
   val equal : t -> t -> bool [@@ocaml.deprecated "Use QConstant.equal"]
   (** Default comparison, alias for [CanOrd.equal] *)
@@ -433,26 +432,7 @@ sig
 
   (** Comparisons *)
 
-  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
+  include QNameS with type t := t
 
   val equal : t -> t -> bool [@@ocaml.deprecated "Use QMutInd.equal"]
  (** Default comparison, alias for [CanOrd.equal] *)
@@ -488,26 +468,7 @@ sig
                                     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
+  include QNameS with type t := t
 
 end
 
@@ -522,26 +483,7 @@ sig
 
   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
+  include QNameS with type t := t
 
 end
 
@@ -642,24 +584,7 @@ module Projection : sig
 
     val make : inductive -> proj_npars:int -> proj_arg:int -> Label.t -> t
 
-    module SyntacticOrd : sig
-      type nonrec t = t
-      val compare : t -> t -> int
-      val equal : t -> t -> bool
-      val hash : t -> int
-    end
-    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
+    include QNameS with type t := t
 
     val constant : t -> Constant.t
     (** Don't use this if you don't have to. *)
@@ -689,18 +614,7 @@ module Projection : sig
   val make : Repr.t -> bool -> t
   val repr : t -> Repr.t
 
-  module SyntacticOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
-  module CanOrd : sig
-    type nonrec t = t
-    val compare : t -> t -> int
-    val equal : t -> t -> bool
-    val hash : t -> int
-  end
+  include QNameS with type t := t
 
   val constant : t -> Constant.t
   val mind : t -> MutInd.t
@@ -745,19 +659,7 @@ module GlobRef : sig
 
   val equal : t -> t -> bool
 
-  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
+  include QNameS with type t := t
 
   module Set_env : CSig.SetS with type elt = t
   module Map_env : Map.ExtS
-- 
cgit v1.2.3


From 70ca8c4f720934049b082de3241a17dea8c9e88f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 14:35:49 +0200
Subject: Introduce the missing dual name quotient modules in Environ.

---
 kernel/environ.ml  | 34 ++++++++++++++++++++++++++++++++--
 kernel/environ.mli | 35 +++++++++++++----------------------
 2 files changed, 45 insertions(+), 24 deletions(-)

diff --git a/kernel/environ.ml b/kernel/environ.ml
index ac7775b89c..17c5a02e2b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -833,13 +833,20 @@ let set_native_symbols env native_symbols = { env with native_symbols }
 let add_native_symbols dir syms env =
   { env with native_symbols = DPmap.add dir syms env.native_symbols }
 
+module type QNameS =
+sig
+  type t
+  val equal : env -> t -> t -> bool
+  val compare : env -> t -> t -> int
+  val hash : env -> t -> int
+end
+
 module QConstant =
 struct
   type t = Constant.t
   let equal _env c1 c2 = Constant.CanOrd.equal c1 c2
   let compare _env c1 c2 = Constant.CanOrd.compare c1 c2
   let hash _env c = Constant.CanOrd.hash c
-  let canonical _env c = (Constant.canonical c)
 end
 
 module QMutInd =
@@ -848,7 +855,22 @@ struct
   let equal _env c1 c2 = MutInd.CanOrd.equal c1 c2
   let compare _env c1 c2 = MutInd.CanOrd.compare c1 c2
   let hash _env c = MutInd.CanOrd.hash c
-  let canonical _env c = (MutInd.canonical c)
+end
+
+module QInd =
+struct
+  type t = Ind.t
+  let equal _env c1 c2 = Ind.CanOrd.equal c1 c2
+  let compare _env c1 c2 = Ind.CanOrd.compare c1 c2
+  let hash _env c = Ind.CanOrd.hash c
+end
+
+module QConstruct =
+struct
+  type t = Construct.t
+  let equal _env c1 c2 = Construct.CanOrd.equal c1 c2
+  let compare _env c1 c2 = Construct.CanOrd.compare c1 c2
+  let hash _env c = Construct.CanOrd.hash c
 end
 
 module QProjection =
@@ -865,3 +887,11 @@ struct
     let hash _env c = Projection.Repr.CanOrd.hash c
   end
 end
+
+module QGlobRef =
+struct
+  type t = GlobRef.t
+  let equal _env c1 c2 = GlobRef.CanOrd.equal c1 c2
+  let compare _env c1 c2 = GlobRef.CanOrd.compare c1 c2
+  let hash _env c = GlobRef.CanOrd.hash c
+end
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 370443857c..f0b40e6492 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -286,39 +286,30 @@ val template_polymorphic_pind : pinductive -> env -> bool
 
 (** {6 Name quotients} *)
 
-module QConstant :
+module type QNameS =
 sig
-  type t = Constant.t
+  type t
   val equal : env -> t -> t -> bool
   val compare : env -> t -> t -> int
   val hash : env -> t -> int
-  val canonical : env -> t -> KerName.t
 end
 
-module QMutInd :
-sig
-  type t = MutInd.t
-  val equal : env -> t -> t -> bool
-  val compare : env -> t -> t -> int
-  val hash : env -> t -> int
-  val canonical : env -> t -> KerName.t
-end
+module QConstant : QNameS with type t = Constant.t
+
+module QMutInd : QNameS with type t = MutInd.t
+
+module QInd : QNameS with type t = Ind.t
+
+module QConstruct : QNameS with type t = Construct.t
 
 module QProjection :
 sig
-  type t = Projection.t
-  val equal : env -> t -> t -> bool
-  val compare : env -> t -> t -> int
-  val hash : env -> t -> int
-  module Repr :
-  sig
-    type t = Projection.Repr.t
-    val equal : env -> t -> t -> bool
-    val compare : env -> t -> t -> int
-    val hash : env -> t -> int
-  end
+  include QNameS with type t = Projection.t
+  module Repr : QNameS with type t = Projection.Repr.t
 end
 
+module QGlobRef : QNameS with type t = GlobRef.t
+
 (** {5 Modules } *)
 
 val add_modtype : module_type_body -> env -> env
-- 
cgit v1.2.3


From 373376b734343d86aecc8d1f91a8c78eefa2b6cc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 14:43:44 +0200
Subject: Document the signatures of quotient names in the API.

---
 kernel/names.mli | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/kernel/names.mli b/kernel/names.mli
index df4ddab3c2..2445d1f309 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -320,9 +320,45 @@ end
 module type QNameS =
 sig
   type t
+  (** A type of reference that implements an implicit quotient by containing
+      two different names. The first one is the user name, i.e. what the user
+      sees when printing. The second one is the canonical name, which is the
+      actual absolute name of the reference.
+
+      This mechanism is fundamentally tied to the module system of Coq. Functor
+      application and module inclusion are the typical ways to introduce names
+      where the canonical and user components differ. In particular, the two
+      components should be undistinguishable from the point of view of typing,
+      i.e. from a "kernel" ground. This aliasing only makes sense inside an
+      environment, but at this point this notion is not even defined so, this
+      dual name trick is fragile. One has to ensure many invariants when
+      creating such names, but the kernel is quite lenient when it comes to
+      checking that these invariants hold. (Read: there are soundness bugs
+      lurking in the module system.)
+
+      One could enforce the invariants by splitting the names and storing that
+      information in the environment instead, but unfortunately, this wreaks
+      havoc in the upper layers. The latter are infamously not stable by
+      syntactic equality, in particular they might observe the difference
+      between canonical and user names if not packed together.
+
+      For this reason, it is discouraged to use the canonical-accessing API
+      in the upper layers, notably the [CanOrd] module below. Instead, one
+      should use their quotiented versions defined in the [Environ] module.
+      Eventually all uses to [CanOrd] outside of the kernel should be removed.
+
+      CAVEAT: name sets and maps are still exposing a canonical-accessing API
+      surreptitiously. *)
+
   module CanOrd : EqType with type t = t
+  (** Equality functions over the canonical name. Their use should be
+      restricted to the kernel. *)
+
   module UserOrd : EqType with type t = t
+  (** Equality functions over the user name. *)
+
   module SyntacticOrd : EqType with type t = t
+  (** Equality functions using both names, for low-level uses. *)
 end
 
 (** {6 Constant Names } *)
-- 
cgit v1.2.3


From 9a3d4e284a03942e8a2b1f9d87a0b349702eaaa9 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 17:56:33 +0200
Subject: Add missing deprecations in Projection API.

---
 kernel/constr.ml             | 6 +++---
 kernel/names.mli             | 4 ++++
 plugins/ssr/ssrequality.ml   | 2 +-
 pretyping/constr_matching.ml | 4 ++--
 pretyping/evarconv.ml        | 2 +-
 pretyping/patternops.ml      | 2 +-
 tactics/cbn.ml               | 2 +-
 7 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/kernel/constr.ml b/kernel/constr.ml
index d538ad7784..3157ec9f57 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -950,7 +950,7 @@ let compare_head_gen_leq_with kind1 kind2 leq_universes leq_sorts eq leq nargs t
     let len = Array.length l1 in
     Int.equal len (Array.length l2) &&
     leq (nargs+len) c1 c2 && Array.equal_norefl (eq 0) l1 l2
-  | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq 0 c1 c2
+  | Proj (p1,c1), Proj (p2,c2) -> Projection.CanOrd.equal p1 p2 && eq 0 c1 c2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && List.equal (eq 0) l1 l2
   | Const (c1,u1), Const (c2,u2) ->
     (* The args length currently isn't used but may as well pass it. *)
@@ -1158,7 +1158,7 @@ let constr_ord_int f t1 t2 =
         ((Int.compare =? (Array.compare f)) ==? (Array.compare f))
         ln1 ln2 tl1 tl2 bl1 bl2
     | CoFix _, _ -> -1 | _, CoFix _ -> 1
-    | Proj (p1,c1), Proj (p2,c2) -> (Projection.compare =? f) p1 p2 c1 c2
+    | Proj (p1,c1), Proj (p2,c2) -> (Projection.CanOrd.compare =? f) p1 p2 c1 c2
     | Proj _, _ -> -1 | _, Proj _ -> 1
     | Int i1, Int i2 -> Uint63.compare i1 i2
     | Int _, _ -> -1 | _, Int _ -> 1
@@ -1456,7 +1456,7 @@ let rec hash t =
     | Meta n -> combinesmall 15 n
     | Rel n -> combinesmall 16 n
     | Proj (p,c) ->
-      combinesmall 17 (combine (Projection.hash p) (hash c))
+      combinesmall 17 (combine (Projection.CanOrd.hash p) (hash c))
     | Int i -> combinesmall 18 (Uint63.hash i)
     | Float f -> combinesmall 19 (Float64.hash f)
     | Array(u,t,def,ty) ->
diff --git a/kernel/names.mli b/kernel/names.mli
index 2445d1f309..9a4ceef802 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -662,14 +662,18 @@ module Projection : sig
   val unfold : t -> t
 
   val equal : t -> t -> bool
+  [@@ocaml.deprecated "Use QProjection.equal"]
   val hash : t -> int
+  [@@ocaml.deprecated "Use QProjection.hash"]
   val hcons : t -> t
   (** Hashconsing of projections. *)
 
   val repr_equal : t -> t -> bool
+  [@@ocaml.deprecated "Use an explicit projection of Repr"]
   (** Ignoring the unfolding boolean. *)
 
   val compare : t -> t -> int
+  [@@ocaml.deprecated "Use QProjection.compare"]
 
   val map : (MutInd.t -> MutInd.t) -> t -> t
   val map_npars : (MutInd.t -> int -> MutInd.t * int) -> t -> t
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 38b26d06b9..a7ebd5f9f5 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -240,7 +240,7 @@ let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with
 
 let same_proj sigma t1 t2 =
   match EConstr.kind sigma t1, EConstr.kind sigma t2 with
-  | Proj(c1,_), Proj(c2, _) -> Projection.equal c1 c2
+  | Proj(c1,_), Proj(c2, _) -> Projection.CanOrd.equal c1 c2
   | _ -> false
 
 let all_ok _ _ = true
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index d394bd1288..a3f1c0b004 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -311,7 +311,7 @@ let matches_core env sigma allow_bound_rels
             || Projection.unfolded pr ->
           raise PatternMatchingFailure
         | PProj (pr1,c1), Proj (pr,c) ->
-          if Projection.equal pr1 pr then
+          if Environ.QProjection.equal env pr1 pr then
             try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c) arg1 arg2
             with Invalid_argument _ -> raise PatternMatchingFailure
           else raise PatternMatchingFailure
@@ -332,7 +332,7 @@ let matches_core env sigma allow_bound_rels
                sorec ctx env subst p term
          with Retyping.RetypeError _ -> raise PatternMatchingFailure)
 
-      | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 ->
+      | PProj (p1,c1), Proj (p2,c2) when Environ.QProjection.equal env p1 p2 ->
           sorec ctx env subst c1 c2
 
       | PProd (na1,c1,d1), Prod(na2,c2,d2) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 1940668519..90af143a2d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -831,7 +831,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
         in
         ise_try evd [f1; f2]
 
-        | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' ->
+        | Proj (p, c), Proj (p', c') when QProjection.Repr.equal env (Projection.repr p) (Projection.repr p') ->
           let f1 i =
             ise_and i
             [(fun i -> evar_conv_x flags env i CONV c c');
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b5c83b75f9..b259945d9e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -59,7 +59,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PCoFix (i1,f1), PCoFix (i2,f2) ->
   Int.equal i1 i2 && rec_declaration_eq f1 f2
 | PProj (p1, t1), PProj (p2, t2) ->
-   Projection.equal p1 p2 && constr_pattern_eq t1 t2
+   Projection.CanOrd.equal p1 p2 && constr_pattern_eq t1 t2
 | PInt i1, PInt i2 ->
    Uint63.equal i1 i2
 | PFloat f1, PFloat f2 ->
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 5838bbcc19..31873ea6b0 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -226,7 +226,7 @@ struct
       match x, y with
       | Cst_const (c1,u1), Cst_const (c2, u2) ->
         Constant.CanOrd.equal c1 c2 && Univ.Instance.equal u1 u2
-      | Cst_proj p1, Cst_proj p2 -> Projection.repr_equal p1 p2
+      | Cst_proj p1, Cst_proj p2 -> Projection.Repr.CanOrd.equal (Projection.repr p1) (Projection.repr p2)
       | _, _ -> false
     in
     let rec equal_rec sk1 sk2 =
-- 
cgit v1.2.3


From 375fc707b402b855770ec32c57ad1362f2a89e5c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 17:53:23 +0200
Subject: Add overlays.

---
 dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh

diff --git a/dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh b/dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh
new file mode 100644
index 0000000000..8b223719ea
--- /dev/null
+++ b/dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "13075" ] || [ "$CI_BRANCH" = "explicit-names-quotient" ]; then
+
+    elpi_CI_REF=explicit-names-quotient
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    coq_dpdgraph_CI_REF=explicit-names-quotient
+    coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph
+
+fi
-- 
cgit v1.2.3