Ajout hashconsing univers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1823 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 0 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 49b2f60728..7c3060820a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -426,3 +426,20 @@ let dump_universes output g =
   in
     UniverseMap.iter dump_arc g 
 
+module Huniv =
+  Hashcons.Make(
+    struct
+      type t = universe
+      type u = string -> string
+      let hash_sub hstr {u_mod=sp; u_num=n} = 
+	{u_mod=List.map hstr sp; u_num=n}
+      let equal {u_mod=sp1; u_num=n1} {u_mod=sp2; u_num=n2} =
+          (List.length sp1 = List.length sp2)
+              & List.for_all2 (==) sp1 sp2 & n1=n2
+      let hash = Hashtbl.hash
+    end)
+
+
+let hcons1_univ u =
+  let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
+  Hashcons.simple_hcons Huniv.f hstring u