- Cleaning phase of the interfaces of libnames.ml and nametab.ml

  (uniformisation of function names, classification). One of the most
  visible change is the renaming of section_path into full_path (the
  use of name section was obsolete due to the module system, but I
  don't know if the new name is the best chosen one - especially it 
  remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.



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

1 files changed, 3 insertions, 3 deletions

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 71f38063a..79b58da84 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -118,7 +118,7 @@ let type_of_global_ref gr =
 let remove_sections dir =
   if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
     (* Not yet (fully) discharged *)
-    Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+    Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ())
   else
     (* Theorem/Lemma outside its outer section of definition *)
     dir
@@ -139,7 +139,7 @@ let add_glob_gen loc sp lib_dp ty =
 
 let add_glob loc ref = 
   if dump () && loc <> Util.dummy_loc then
-    let sp = Nametab.sp_of_global ref in
+    let sp = Nametab.path_of_global ref in
     let lib_dp = Lib.library_part ref in
     let ty = type_of_global_ref ref in
       add_glob_gen loc sp lib_dp ty
@@ -150,7 +150,7 @@ let mp_of_kn kn =
 
 let add_glob_kn loc kn =
   if dump () && loc <> Util.dummy_loc then
-    let sp = Nametab.sp_of_syntactic_definition kn in
+    let sp = Nametab.path_of_syndef kn in
     let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
       add_glob_gen loc sp lib_dp "syndef"