*** empty log message ***

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

5 files changed, 28 insertions, 28 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 6999ee669..d5dc01cf5 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -431,7 +431,7 @@ let strength_of_global = function
   | IndRef _ | ConstructRef _ | ConstRef _ -> Global
 
 let library_part ref =
-  let sp = Nametab.sp_of_global None ref in
+  let sp = Nametab.sp_of_global ref in
   let dir,_ = repr_path sp in
   match strength_of_global ref with
   | Local -> 
diff --git a/library/goptions.ml b/library/goptions.ml
index 4c2d15206..b1868fdd7 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -309,7 +309,7 @@ let msg_option_value (name,v) =
     | IntValue (Some n) -> int n
     | IntValue None   -> str "undefined"
     | StringValue s   -> str s
-    | IdentValue r    -> pr_global_env None r
+    | IdentValue r    -> pr_global_env Idset.empty r
 
 let print_option_value key =
   let (name,(_,read,_)) = get_option key in
diff --git a/library/library.mli b/library/library.mli
index d1d345aab..d69ecef9e 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -46,7 +46,7 @@ val require_library :
   bool option -> qualid located list -> bool -> unit
 
 val require_library_from_file :
-  bool option -> identifier option -> string -> bool -> unit
+  bool option -> identifier option -> System.physical_path -> bool -> unit
 
 (*s [save_library_to s f] saves the current environment as a library [s]
   in the file [f]. *)
diff --git a/library/nametab.ml b/library/nametab.ml
index cbb3b23e9..372590911 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -70,7 +70,7 @@ module type NAMETREE = sig
   val find : user_name -> 'a t -> 'a
   val exists : user_name -> 'a t -> bool
   val user_name : qualid -> 'a t -> user_name
-  val shortest_qualid : user_name -> 'a t -> qualid
+  val shortest_qualid : Idset.t -> user_name -> 'a t -> qualid
 end
 
 module Make(U:UserName) : NAMETREE with type user_name = U.t 
@@ -207,15 +207,17 @@ let exists uname tab =
   with
       Not_found -> false
 
-let shortest_qualid uname tab = 
+let shortest_qualid ctx uname tab = 
+  let id,dir = U.repr uname in
+  let hidden = Idset.mem id ctx in
   let rec find_uname pos dir (path,tab) = match path with
-    | Absolute (u,_) | Relative (u,_) when u=uname -> List.rev pos 
+    | Absolute (u,_) | Relative (u,_)
+          when u=uname && not(pos=[] && hidden) -> List.rev pos 
     | _ -> 
 	match dir with 
 	    [] -> raise Not_found
 	  | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tab)
   in
-  let id,dir = U.repr uname in
   let ptab = Idmap.find id tab in
   let found_dir = find_uname [] dir ptab in
     make_qualid (make_dirpath found_dir) id
@@ -413,16 +415,14 @@ let exists_modtype sp = SpTab.exists sp !the_modtypetab
 
 (* Reverse locate functions ***********************************************)
 
-let sp_of_global ctx_opt ref = 
-  match (ctx_opt,ref) with
-    | Some ctx, VarRef id -> 
-	let _ = Sign.lookup_named id ctx in
-	  make_path empty_dirpath id
+let sp_of_global ref = 
+  match ref with
+    | VarRef id -> make_path empty_dirpath id
     | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
 
 
-let id_of_global ctx_opt ref = 
-  let (_,id) = repr_path (sp_of_global ctx_opt ref) in 
+let id_of_global ref = 
+  let (_,id) = repr_path (sp_of_global ref) in 
   id
 
 let sp_of_syntactic_definition kn = 
@@ -434,21 +434,24 @@ let dir_of_mp mp =
 
 (* Shortest qualid functions **********************************************)
 
-let shortest_qualid_of_global ctx_opt ref = 
-  let sp = sp_of_global ctx_opt ref in
-    SpTab.shortest_qualid sp !the_ccitab
+let shortest_qualid_of_global ctx ref = 
+  match ref with
+    | VarRef id -> make_qualid empty_dirpath id
+    | _ ->
+        let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
+        SpTab.shortest_qualid ctx sp !the_ccitab
 
 let shortest_qualid_of_syndef kn = 
   let sp = sp_of_syntactic_definition kn in
-    SpTab.shortest_qualid sp !the_ccitab
+    SpTab.shortest_qualid Idset.empty sp !the_ccitab
 
 let shortest_qualid_of_module mp = 
   let dir = MPmap.find mp !the_modrevtab in
-    DirTab.shortest_qualid dir !the_dirtab
+    DirTab.shortest_qualid Idset.empty dir !the_dirtab
 
 let shortest_qualid_of_modtype kn =
   let sp = KNmap.find kn !the_modtyperevtab in
-    SpTab.shortest_qualid sp !the_modtypetab
+    SpTab.shortest_qualid Idset.empty sp !the_modtypetab
 
 let pr_global_env env ref =
   (* Il est important de laisser le let-in, car les streams s'évaluent
diff --git a/library/nametab.mli b/library/nametab.mli
index f14b1a123..9ee45a9ad 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -133,23 +133,20 @@ val full_name_module : qualid -> dir_path
 (*s Reverse lookup -- finding user names corresponding to the given
   internal name *)
 
-
 val sp_of_syntactic_definition : kernel_name -> section_path
-
-val sp_of_global : 
-  Sign.named_context option -> global_reference -> section_path
 val shortest_qualid_of_global : 
-  Sign.named_context option -> global_reference -> qualid
+  Idset.t -> global_reference -> qualid
 val shortest_qualid_of_syndef : 
   kernel_name -> qualid
-val id_of_global : 
-  Sign.named_context option -> global_reference -> identifier
 
 val dir_of_mp :
   module_path -> dir_path
 
+val sp_of_global : global_reference -> section_path
+val id_of_global : global_reference -> identifier
+
 (* Printing of global references using names as short as possible *)
-val pr_global_env : Sign.named_context option -> global_reference -> std_ppcmds
+val pr_global_env : Idset.t -> global_reference -> std_ppcmds
 
 
 (* The [shortest_qualid] functions given an object with user_name