From 8fafc201699e3d6c80e39bbadf2e6a5ba6425036 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 17:17:19 +0200
Subject: Move maps & sets indexed by GlobRef.t into the kernel

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

(limited to 'kernel/names.mli')

diff --git a/kernel/names.mli b/kernel/names.mli
index 1cdf5c2402..2ea8108734 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -645,6 +645,28 @@ module GlobRef : sig
 
   val equal : t -> t -> bool
 
+  module Ordered : sig
+    type nonrec t = t
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
+  module Ordered_env : sig
+    type nonrec t = t
+    val compare : t -> t -> int
+    val equal : t -> t -> bool
+    val hash : t -> int
+  end
+
+  module Set_env : CSig.SetS with type elt = t
+  module Map_env : Map.ExtS
+    with type key = t and module Set := Set_env
+
+  module Set : CSig.SetS with type elt = t
+  module Map : Map.ExtS
+    with type key = t and module Set := Set
+
 end
 
 type global_reference = GlobRef.t
-- 
cgit v1.2.3