From ffa57bae1e18fd52d63e8512a352ac63db15a7a9 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 6 Aug 2009 19:00:11 +0000 Subject: - 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 --- interp/dumpglob.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp/dumpglob.ml') 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" -- cgit v1.2.3