Ajout sp_of_global; Introduction constant_path = section_path

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

2 files changed, 15 insertions, 8 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index d95a872536..ed74f0f2d8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -202,20 +202,24 @@ let lookup_mind sp env =
 let lowercase_first_char id = String.lowercase (first_char id)
 
 (* id_of_global gives the name of the given sort oper *)
-let id_of_global env = function
-  | ConstRef sp -> 
-      basename sp
+let sp_of_global env = function
+  | VarRef sp -> sp
+  | ConstRef sp -> sp
   | IndRef (sp,tyi) -> 
       (* Does not work with extracted inductive types when the first 
 	 inductive is logic : if tyi=0 then basename sp else *)
       let mib = lookup_mind sp env in
       let mip = mind_nth_type_packet mib tyi in
-      mip.mind_typename
+      make_path (dirpath sp) mip.mind_typename CCI
   | ConstructRef ((sp,tyi),i) ->
       let mib = lookup_mind sp env in
       let mip = mind_nth_type_packet mib tyi in
       assert (i <= Array.length mip.mind_consnames && i > 0);
-      mip.mind_consnames.(i-1)
+      make_path (dirpath sp) mip.mind_consnames.(i-1) CCI
+  | EvarRef n -> 
+      make_path [] (id_of_string ("?"^(string_of_int n))) CCI
+
+let id_of_global env ref = basename (sp_of_global env ref)
 
 let hdchar env c = 
   let rec hdrec k c =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 84f384759c..7e90dd4cd0 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -94,13 +94,16 @@ val lookup_rel_value : int -> env -> constr option
 
 (* Looks up in the context of global constant names *)
 (* raises [Not_found] if the required path is not found *)
-val lookup_constant : section_path -> env -> constant_body
+val lookup_constant : constant_path -> env -> constant_body
 
 (* Looks up in the context of global inductive names *)
 (* raises [Not_found] if the required path is not found *)
 val lookup_mind : section_path -> env -> mutual_inductive_body
 
 (*s Miscellanous *)
+
+val sp_of_global : env -> global_reference -> section_path
+
 val id_of_global : env -> global_reference -> identifier
 
 val make_all_name_different : env -> env
@@ -146,8 +149,8 @@ val evaluable_constant : env -> constant -> bool
 
 (*s Opaque / Transparent switching *)
 
-val set_opaque : env -> section_path -> unit
-val set_transparent : env -> section_path -> unit
+val set_opaque : env -> constant_path -> unit
+val set_transparent : env -> constant_path -> unit
 
 (*s Modules. *)