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(+)

(limited to 'kernel')

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.
---
 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 ++--
 12 files changed, 31 insertions(+), 24 deletions(-)

(limited to 'kernel')

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)
-- 
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 +-
 6 files changed, 22 insertions(+), 9 deletions(-)

(limited to 'kernel')

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
 
-- 
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.

---
 kernel/names.ml  | 8 ++++----
 kernel/names.mli | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'kernel')

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
-- 
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.
---
 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 +-
 14 files changed, 152 insertions(+), 89 deletions(-)

(limited to 'kernel')

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)
-- 
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.

---
 kernel/constr.ml       |  10 ++---
 kernel/cooking.ml      |   4 +-
 kernel/names.ml        | 103 ++++++++++++++++++++++++++++++-------------------
 kernel/names.mli       |  47 ++++++++++++++++++++--
 kernel/nativelambda.ml |   4 +-
 5 files changed, 115 insertions(+), 53 deletions(-)

(limited to 'kernel')

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)
-- 
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(-)

(limited to 'kernel')

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(-)

(limited to 'kernel')

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(+)

(limited to 'kernel')

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 ++++
 2 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3