diff options
author | 2009-08-06 19:00:11 +0000 | |
---|---|---|
committer | 2009-08-06 19:00:11 +0000 | |
commit | ffa57bae1e18fd52d63e8512a352ac63db15a7a9 (patch) | |
tree | 6cf537ce557f14f71ee3693d98dc20c12b64a9e4 /library/library.ml | |
parent | da7fb3e13166747b49cdf1ecfad394ecb4e0404a (diff) |
- 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
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/library.ml b/library/library.ml index abca3c7e7..24c2c3803 100644 --- a/library/library.ml +++ b/library/library.ml @@ -308,7 +308,7 @@ let subst_import (_,_,o) = o let export_import o = Some o -let classify_import (_,(_,export as obj)) = +let classify_import (_,export as obj) = if export then Substitute obj else Dispose @@ -367,7 +367,7 @@ let locate_qualified_library warn qid = if loadpath = [] then raise LibUnmappedDir; let name = string_of_id base ^ ".vo" in let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in - let dir = extend_dirpath (List.assoc lpath loadpath) base in + let dir = add_dirpath_suffix (List.assoc lpath loadpath) base in (* Look if loaded *) if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) (* Otherwise, look for it in the file system *) @@ -540,7 +540,7 @@ let (in_require, out_require) = open_function = (fun _ _ -> assert false); export_function = export_require; discharge_function = discharge_require; - classify_function = (fun (_,o) -> Anticipate o) } + classify_function = (fun o -> Anticipate o) } (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) @@ -615,7 +615,7 @@ let start_library f = let ldir0 = find_logical_path (Filename.dirname longf) in let id = id_of_string (Filename.basename f) in check_coq_overwriting ldir0 id; - let ldir = extend_dirpath ldir0 id in + let ldir = add_dirpath_suffix ldir0 id in Declaremods.start_library ldir; ldir,longf |