Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 28 insertions, 19 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 08e9fee0..763c0822 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -194,7 +194,17 @@ struct
     | Level _, _ -> -1
     | _, Level _ -> 1
     | Var n, Var m -> Int.compare n m
-      
+
+  let hequal x y =
+    x == y ||
+      match x, y with
+      | Prop, Prop -> true
+      | Set, Set -> true
+      | Level (n,d), Level (n',d') ->
+        n == n' && d == d'
+      | Var n, Var n' -> n == n'
+      | _ -> false
+
   let hcons = function
     | Prop as x -> x
     | Set as x -> x
@@ -233,27 +243,26 @@ module Level = struct
 
   let hash x = x.hash
 
-  let hcons x = 
-    let data' = RawLevel.hcons x.data in
-      if data' == x.data then x
-      else { x with data = data' }
-
   let data x = x.data
 
   (** Hashcons on levels + their hash *)
 
-  let make =
-    let module Self = struct
-      type _t = t
-      type t = _t
-      let equal = equal
-      let hash = hash
-    end in
-    let module WH = Weak.Make(Self) in
-    let pool = WH.create 4910 in fun x ->
-    let x = { hash = RawLevel.hash x; data = x } in
-    try WH.find pool x
-    with Not_found -> WH.add pool x; x
+  module Self = struct
+    type _t = t
+    type t = _t
+    type u = unit
+    let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+    let hash x = x.hash
+    let hashcons () x =
+      let data' = RawLevel.hcons x.data in
+      if x.data == data' then x else { x with data = data' }
+  end
+
+  let hcons =
+    let module H = Hashcons.Make(Self) in
+    Hashcons.simple_hcons H.generate H.hcons ()
+
+  let make l = hcons { hash = RawLevel.hash l; data = l }
 
   let set = make Set
   let prop = make Prop
@@ -2064,7 +2073,7 @@ let explain_universe_inconsistency prl (o,u,v,p) =
 	    (spc() ++ str "= " ++ pr_uni u)) 
   in
     str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
-      pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")"
+      pr_rel o ++ spc() ++ pr_uni v ++ reason
 
 let compare_levels = Level.compare
 let eq_levels = Level.equal