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 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

(limited to 'kernel/environ.ml')

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
-- 
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 ++++++++++++++++++++++++++++++++--
 1 file changed, 32 insertions(+), 2 deletions(-)

(limited to 'kernel/environ.ml')

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