Ajout hashconsing univers

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

1 files changed, 24 insertions, 3 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 1f68c1a359..075b3dbad5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1733,11 +1733,27 @@ module Htype =
       let hash = Hashtbl.hash
     end)
 
-let hsort _ _ s = s
+module Hsorts =
+  Hashcons.Make(
+    struct
+      type t = sorts
+      type u = universe -> universe
+      let hash_sub huniv = function
+          Prop c -> Prop c
+        | Type u -> Type (huniv u)
+      let equal s1 s2 =
+        match (s1,s2) with
+            (Prop c1, Prop c2) -> c1=c2
+          | (Type u1, Type u2) -> u1 == u2
+          |_ -> false
+      let hash = Hashtbl.hash
+    end)
+
+let hsort = Hsorts.f
 
 let hcons_constr (hspcci,hspfw,hname,hident,hstr) =
-  let hsortscci = Hashcons.simple_hcons hsort hspcci in
-  let hsortsfw = Hashcons.simple_hcons hsort hspfw in
+  let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in
+  let hsortsfw = Hashcons.simple_hcons hsort hcons1_univ in
   let hcci = hcons_term (hsortscci,hspcci,hname,hident) in
   let hfw = hcons_term (hsortsfw,hspfw,hname,hident) in
   let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
@@ -1748,6 +1764,11 @@ let hcons1_constr =
   let (hc,_,_) = hcons_constr hnames in
   hc
 
+let hcons1_types =
+  let hnames = hcons_names () in
+  let (_,_,ht) = hcons_constr hnames in
+  ht
+
 (* Abstract decomposition of constr to deal with generic functions *)
 
 type fix_kind = RFix of (int array * int) | RCoFix of int