Fix the hconsing of universes

 Two issues were preventing the hcons1_univ function to properly work

  - a launch of Names.hcons_names () at each hconsing of universe,
    hence one separated hash-table for dir-path created at each time,
    oups...

  - Bad handling of the universe sub-structure universe_level

 To check : is there an interest in making separate calls to
 Names.hcons_names () in separate places (Univ, Term, Declare) ?
 I think not. Btw the hconsing of Declare.hcons_constant_declaration
 is also probably wrong. To be fixed in a forthcoming patch.

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

1 files changed, 26 insertions, 8 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 660e39e63..32e08abd8 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -824,18 +824,30 @@ let dump_universes output g =
 
 (* Hash-consing *)
 
-module Huniv =
+module Hunivlevel =
   Hashcons.Make(
     struct
-      type t = universe
+      type t = universe_level
       type u = Names.dir_path -> Names.dir_path
-      let hash_aux hdir = function
+      let hash_sub hdir = function
 	| UniverseLevel.Set -> UniverseLevel.Set
 	| UniverseLevel.Level (d,n) -> UniverseLevel.Level (hdir d,n)
+      let equal l1 l2 = match l1,l2 with
+	| UniverseLevel.Set, UniverseLevel.Set -> true
+	| UniverseLevel.Level (d,n), UniverseLevel.Level (d',n') ->
+	  n == n' && d == d'
+	| _ -> false
+      let hash = Hashtbl.hash
+    end)
+
+module Huniv =
+  Hashcons.Make(
+    struct
+      type t = universe
+      type u = universe_level -> universe_level
       let hash_sub hdir = function
-	| Atom u -> Atom (hash_aux hdir u)
-	| Max (gel,gtl) ->
-	    Max (List.map (hash_aux hdir) gel, List.map (hash_aux hdir) gtl)
+	| Atom u -> Atom (hdir u)
+	| Max (gel,gtl) -> Max (List.map hdir gel, List.map hdir gtl)
       let equal u v =
 	match u, v with
 	  | Atom u, Atom v -> u == v
@@ -846,7 +858,13 @@ module Huniv =
       let hash = Hashtbl.hash
     end)
 
-let hcons1_univ u =
+let hcons1_univlevel =
+  (* Beware: it is important to run the next line at launch-time
+     since it creates internal hash-tables.
+     We could/should probably share the other calls to [hcons_names]
+     in Term and Declare *)
   let _,_,hdir,_,_,_ = Names.hcons_names() in
-  Hashcons.simple_hcons Huniv.f hdir u
+  Hashcons.simple_hcons Hunivlevel.f hdir
+
+let hcons1_univ = Hashcons.simple_hcons Huniv.f hcons1_univlevel