Modules dans COQ\!\!\!\!

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

1 files changed, 12 insertions, 11 deletions

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 7f77bcdba..05411c68d 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -15,6 +15,7 @@ open Nameops
 open Term
 open Sign
 open Environ
+open Libnames
 open Nametab
 
 let print_sort = function
@@ -27,15 +28,15 @@ let print_sort_family = function
   | InProp -> (str "Prop")
   | InType -> (str "Type")
 
-let current_module = ref empty_dirpath
+(*let current_module = ref empty_dirpath
 
-let set_module m = current_module := m
+let set_module m = current_module := m*)
 
 let new_univ = 
   let univ_gen = ref 0 in
   (fun sp ->
     incr univ_gen; 
-    Univ.make_univ (!current_module,!univ_gen))
+    Univ.make_univ (Lib.module_dp(),!univ_gen))
 
 let new_sort_in_family = function 
   | InProp -> mk_Prop
@@ -510,7 +511,7 @@ let first_char id =
 
 let lowercase_first_char id = String.lowercase (first_char id)
 
-let id_of_global env ref = basename (sp_of_global env ref)
+let id_of_global env ref = Nametab.id_of_global (Some (named_context env)) ref
 
 let sort_hdchar = function
   | Prop(_) -> "P"
@@ -524,12 +525,12 @@ let hdchar env c =
     | LetIn (_,_,_,c)    -> hdrec (k+1) c
     | Cast (c,_)         -> hdrec k c
     | App (f,l)         -> hdrec k f
-    | Const sp       ->
-	let c = lowercase_first_char (basename sp) in
+    | Const kn       ->
+	let c = lowercase_first_char (id_of_label (label kn)) in
 	if c = "?" then "y" else c
-    | Ind ((sp,i) as x) ->
+    | Ind ((kn,i) as x) ->
 	if i=0 then 
-	  lowercase_first_char (basename sp)
+	  lowercase_first_char (id_of_label (label kn))
 	else 
 	  lowercase_first_char (id_of_global env (IndRef x))
     | Construct ((sp,i) as x) ->
@@ -644,12 +645,12 @@ let occur_rel p env id =
 let occur_id env nenv id0 c =
   let rec occur n c = match kind_of_term c with
     | Var id when  id=id0 -> raise Occur
-    | Const sp when basename sp = id0 -> raise Occur
+    | Const kn when id_of_global env (ConstRef kn) = id0 -> raise Occur
     | Ind ind_sp
-	when basename (path_of_inductive env ind_sp) = id0 ->
+	when id_of_global env (IndRef ind_sp) = id0 ->
         raise Occur
     | Construct cstr_sp
-	when basename (path_of_constructor env cstr_sp) = id0 ->
+	when id_of_global env (ConstructRef cstr_sp) = id0 ->
         raise Occur
     | Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur
     | _ -> iter_constr_with_binders succ occur n c