Introduce the missing dual name quotient modules in Environ.

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