Déplacement de Declare juste à la fin de interp pour pouvoir accéder à interp

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

4 files changed, 19 insertions, 20 deletions

diff --git a/library/declare.mli b/library/declare.mli
index 27778884f..14540532b 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -90,27 +90,8 @@ val clear_proofs : named_context -> named_context
 (*s Global references *)
 
 val context_of_global_reference : global_reference -> section_context
-
-val global_qualified_reference : qualid -> constr
-val global_absolute_reference : section_path -> constr
-val global_reference_in_absolute_module : dir_path -> identifier -> constr
-
-val construct_qualified_reference : qualid -> constr
-val construct_absolute_reference : section_path -> constr
-
-(* This should eventually disappear *)
-(*  [construct_reference] returns the object corresponding to
-    the name [id] in the global environment. It looks also for variables in a 
-    given environment instead of looking in the current global environment. *)
-val global_reference : identifier -> constr
-val construct_reference : Sign.named_context option -> identifier -> constr
-
-val is_global : identifier -> bool
-
 val strength_of_global : global_reference -> strength
 
-val library_part : global_reference -> dir_path
-
 (* hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
 val set_xml_declare_constant : (object_name -> unit) -> unit
diff --git a/library/lib.ml b/library/lib.ml
index f24cf4892..179e51bf8 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -525,3 +525,19 @@ let reset_initial () =
 	end
 
 
+(* Misc *)
+
+let library_part ref =
+  let sp = Nametab.sp_of_global ref in
+  let dir,_ = repr_path sp in
+  match ref with
+  | VarRef id -> 
+      anomaly "TODO";
+      extract_dirpath_prefix (sections_depth ()) (cwd ())
+  | _ ->
+      if is_dirpath_prefix_of dir (cwd ()) then
+        (* Not yet (fully) discharged *)
+        extract_dirpath_prefix (sections_depth ()) (cwd ())
+      else
+	(* Theorem/Lemma outside its outer section of definition *)
+	dir
diff --git a/library/lib.mli b/library/lib.mli
index 2f51d441d..e16f44af8 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -117,6 +117,9 @@ val end_compilation : dir_path -> object_prefix * library_segment
    compiling library (or [default_library]) *)
 val library_dp : unit -> dir_path
 
+(* Extract the library part of a name even if in a section *)
+val library_part : global_reference -> dir_path
+
 (*s Sections *)
 
 val open_section : identifier -> object_prefix
diff --git a/library/libnames.ml b/library/libnames.ml
index 03d16f417..e8da68087 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -267,4 +267,3 @@ let pr_reference = function
 let loc_of_reference = function
   | Qualid (loc,qid) -> loc
   | Ident (loc,id) -> loc
-