correction bug univers (dummy_univ)

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

4 files changed, 30 insertions, 39 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f1b97bcd22..75e7cd70df 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -90,7 +90,8 @@ let rec execute mf env cstr =
 	(judge_of_prop_contents c, cst0)
 
     | IsSort (Type u) ->
-	judge_of_type u
+	let inst_u = if u == dummy_univ then new_univ() else u in
+	judge_of_type inst_u
 	  
     | IsApp (f,args) ->
 	let (j,cst1) = execute mf env f in
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
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0f6b7185ae..f179bd3704 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -15,27 +15,30 @@
 
 open Pp
 open Util
-open Names
 
-type universe = { u_sp : section_path; u_num : int }
+type universe = { u_mod : string; u_num : int }
 
 let universe_ord x y =
   let c = x.u_num - y.u_num in
-  if c <> 0 then c else sp_ord x.u_sp y.u_sp
+  if c <> 0 then c else compare x.u_mod y.u_mod
   
 module UniverseOrdered = struct
   type t = universe
   let compare = universe_ord
 end
 
-let pr_uni u = [< 'sTR(string_of_path u.u_sp) ; 'sTR"." ; 'iNT u.u_num >]
+let pr_uni u = [< 'sTR u.u_mod ; 'sTR"." ; 'iNT u.u_num >]
 
-let dummy_sp = make_path ["univ"] (id_of_string "dummy") OBJ
-let dummy_univ = {u_sp = dummy_sp; u_num = 0} (* for prover terms *)
+let dummy_univ = { u_mod = "dummy univ"; u_num = 0 } (* for prover terms *)
+let implicit_univ = { u_mod = "implicit univ"; u_num = 0 }
+
+let current_module = ref ""
+
+let set_module m = current_module := m
 
 let new_univ = 
   let univ_gen = ref 0 in
-  (fun sp -> incr univ_gen; { u_sp = sp; u_num = !univ_gen })
+  (fun sp -> incr univ_gen; { u_mod = !current_module; u_num = !univ_gen })
 
 type relation = 
   | Greater of bool * universe * relation (* if bool then > else >= *)
@@ -65,10 +68,10 @@ let declare_univ u g =
 (* The universes of Prop and Set: Type_0, Type_1 and Type_2, and the
    resulting graph. *)
 let (initial_universes,prop_univ,prop_univ_univ,prop_univ_univ_univ) =
-  let prop_sp = make_path ["univ"] (id_of_string "prop_univ") OBJ in
-  let u = { u_sp = prop_sp; u_num = 0 } in
-  let su = { u_sp = prop_sp; u_num = 1 } in
-  let ssu = { u_sp = prop_sp; u_num = 2 } in
+  let prop_sp = "prop_univ" in
+  let u = { u_mod = prop_sp; u_num = 0 } in
+  let su = { u_mod = prop_sp; u_num = 1 } in
+  let ssu = { u_mod = prop_sp; u_num = 2 } in
   let g = enter_arc (Arc(u,Terminal)) UniverseMap.empty in
   let g = enter_arc (Arc(su,Terminal)) g in
   let g = enter_arc (Arc(ssu,Terminal)) g in
@@ -342,7 +345,7 @@ let sup u v g =
     | NGE -> 
 	(match compare g v u with
            | NGE -> 
-	       let w = new_univ u.u_sp in
+	       let w = new_univ () in
 	       let c = Constraint.add (w,Geq,u) 
 			 (Constraint.singleton (w,Geq,v)) in
 	       w, c
@@ -358,7 +361,7 @@ let super u =
   else if u == prop_univ_univ then 
     prop_univ_univ_univ, Constraint.empty
   else
-    let v = new_univ u.u_sp in
+    let v = new_univ () in
     let c = Constraint.singleton (v,Gt,u) in
     v,c
 
@@ -366,11 +369,11 @@ let super_super u =
   if u == prop_univ then
     prop_univ_univ, prop_univ_univ_univ, Constraint.empty
   else if u == prop_univ_univ then 
-    let v = new_univ u.u_sp in
+    let v = new_univ () in
     prop_univ_univ_univ, v, Constraint.singleton (v,Gt,prop_univ_univ_univ)
   else
-    let v = new_univ u.u_sp in
-    let w = new_univ u.u_sp in
+    let v = new_univ () in
+    let w = new_univ () in
     let c = Constraint.add (w,Gt,v) (Constraint.singleton (v,Gt,u)) in
     v, w, c
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 65468be3cb..c69b809bbc 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -7,15 +7,18 @@ open Names
 
 (* Universes. *)
 
-type universe = { u_sp : section_path; u_num : int }
+type universe
 
 val dummy_univ : universe
+val implicit_univ : universe
 
 val prop_univ : universe
 val prop_univ_univ : universe
 val prop_univ_univ_univ : universe
 
-val new_univ : section_path -> universe
+val set_module : string -> unit
+
+val new_univ : unit -> universe
 
 (*s Graphs of universes. *)