correction bug univers (dummy_univ)

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

1 files changed, 4 insertions, 20 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 9e3ed34797..5c045a8ab0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1141,8 +1141,7 @@ let mkFix = mkFix
 let mkCoFix = mkCoFix
 
 (* Construct an implicit *)
-let implicit_univ = make_path ["Implicit"] (id_of_string "dummy") OBJ
-let implicit_sort = Type { u_sp = implicit_univ ; u_num = 0}
+let implicit_sort = Type implicit_univ
 let mkImplicit = mkSort implicit_sort
 
 let rec strip_outer_cast c = match kind_of_term c with
@@ -1668,26 +1667,11 @@ module Htype =
       let hash = Hashtbl.hash
     end)
 
-module Hsorts =
-  Hashcons.Make(
-    struct
-      type t = sorts
-      type u = section_path -> section_path
-      let hash_sub hsp = function
-	| Prop c -> Prop c
-        | Type {u_sp=sp; u_num=n} -> Type {u_sp=hsp sp; u_num=n}
-      let equal s1 s2 =
-        match (s1,s2) with
-          | (Prop c1, Prop c2) -> c1=c2
-          | (Type {u_sp=sp1; u_num=n1}, Type {u_sp=sp2; u_num=n2}) ->
-              sp1==sp2 & n1=n2
-          |_ -> false
-      let hash = Hashtbl.hash
-    end)
+let hsort _ _ s = s
 
 let hcons_constr (hspcci,hspfw,hname,hident,hstr) =
-  let hsortscci = Hashcons.simple_hcons Hsorts.f hspcci in
-  let hsortsfw = Hashcons.simple_hcons Hsorts.f hspfw in
+  let hsortscci = Hashcons.simple_hcons hsort hspcci in
+  let hsortsfw = Hashcons.simple_hcons hsort hspfw in
   let hcci = hcons_term (hsortscci,hspcci,hname,hident,hstr) in
   let hfw = hcons_term (hsortsfw,hspfw,hname,hident,hstr) in
   let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in