diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-28 11:04:59 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-28 11:04:59 +0200 |
commit | 2cf609c41f7af83d9eaf43308a368fcb7307e6fa (patch) | |
tree | cdc9a1459d4b753309d7ad729bf41c7f50522adb /library/library.ml | |
parent | b6d5a9f47634371aa18c6e3159c6bc24203d229f (diff) |
Make -load-vernac-object respect the loadpath.
This command-line option was behaving like the old -require, except that
it did not do Import. In other words, it was loading files without
respecting the loadpath. Now it behaves exactly like Require, while
-require now behaves like Require Import.
This patch also removes Library.require_library_from_file and all its
dependencies, since they are no longer used inside Coq.
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/library/library.ml b/library/library.ml index a09f91b15..6d7b0f603 100644 --- a/library/library.ml +++ b/library/library.ml @@ -488,33 +488,11 @@ let rec_intern_library libs mref = let _, libs = intern_library libs mref None in libs -let rec_intern_by_filename_only f = - let m = try intern_from_file f with Sys_error s -> error s in - (* We check no other file containing same library is loaded *) - if library_is_loaded m.library_name then - begin - msg_warning - (pr_dirpath m.library_name ++ str " is already loaded from file " ++ - str (library_full_filename m.library_name)); - m.library_name, [] - end - else - let needed, contents = intern_library_deps ([], DPMap.empty) m.library_name m (Some f) in - let needed = List.map (fun dir -> dir, DPMap.find dir contents) needed in - m.library_name, needed - let native_name_from_filename f = let ch = System.with_magic_number_check raw_intern_library f in let (lmd : seg_sum), pos, digest_lmd = System.marshal_in_segment f ch in Nativecode.mod_uid_of_dirpath lmd.md_name -let rec_intern_library_from_file f = - (* A name is specified, we have to check it contains library id *) - let paths = Loadpath.get_paths () in - let _, f = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in - rec_intern_by_filename_only f - (**********************************************************************) (*s [require_library] loads and possibly opens a library. This is a synchronized operation. It is performed as follows: @@ -590,18 +568,6 @@ let require_library_from_dirpath modrefl export = add_anonymous_leaf (in_require (needed,modrefl,export)); add_frozen_state () -let require_library_from_file file export = - let modref,needed = rec_intern_library_from_file file in - let needed = List.rev_map snd needed in - if Lib.is_module_or_modtype () then begin - add_anonymous_leaf (in_require (needed,[modref],None)); - Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp))) - export - end - else - add_anonymous_leaf (in_require (needed,[modref],export)); - add_frozen_state () - (* the function called by Vernacentries.vernac_import *) let safe_locate_module (loc,qid) = |