Using HMaps in global references.

2 files changed, 7 insertions, 0 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 50402eb837..6b433c4823 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -561,6 +561,8 @@ let ind_user_ord (m1, i1) (m2, i2) =
   if Int.equal c 0 then MutInd.UserOrd.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 eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
 let constructor_ord (ind1, j1) (ind2, j2) =
@@ -571,6 +573,8 @@ let constructor_user_ord (ind1, j1) (ind2, j2) =
   if Int.equal c 0 then ind_user_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)
 
 module InductiveOrdered = struct
   type t = inductive
diff --git a/kernel/names.mli b/kernel/names.mli
index a9da13399e..b2a3631743 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -243,6 +243,7 @@ sig
   (** Comparisons *)
   val compare : t -> t -> int
   val equal : t -> t -> bool
+  val hash : t -> int
 end
 
 module KNset  : CSig.SetS with type elt = KerName.t
@@ -412,10 +413,12 @@ val eq_ind : inductive -> inductive -> bool
 val ind_ord : inductive -> inductive -> int
 val ind_hash : inductive -> int
 val ind_user_ord : inductive -> inductive -> int
+val ind_user_hash : inductive -> int
 val eq_constructor : constructor -> constructor -> bool
 val constructor_ord : constructor -> constructor -> int
 val constructor_user_ord : constructor -> constructor -> int
 val constructor_hash : constructor -> int
+val constructor_user_hash : constructor -> int
 
 (** Better to have it here that in Closure, since required in grammar.cma *)
 type evaluable_global_reference =