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.

7 files changed, 16 insertions, 47 deletions

diff --git a/CHANGES b/CHANGES
index 950f2fab1..16d86c8ff 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,8 +54,9 @@ Tools
 - The -compile command-line option now takes the full path of the considered
   file, including the ".v" extension, and outputs a warning if such an extension
   is lacking.
-- The -require command-line option now takes a logical path of a given library
-  rather than a physical path.
+- The -require and -load-vernac-object command-line options now take a logical
+  path of a given library rather than a physical path, thus they behave like
+  Require [Import] path.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 0f1823a02..9862abb53 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -153,9 +153,9 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
   Load \Coq~file {\em file}{\tt .v} optionally with copy it contents on the
   standard input.
 
-\item[{\tt -load-vernac-object} {\em file}]\ 
+\item[{\tt -load-vernac-object} {\em path}]\ 
 
-  Load \Coq~compiled file {\em file}{\tt .vo}
+  Load \Coq~compiled library {\em path} (equivalent to {\tt Require} {\em path}).
 
 \item[{\tt -require} {\em path}]\ 
 
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) =
diff --git a/library/library.mli b/library/library.mli
index 3d96f9a75..d5e610dd6 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -22,7 +22,6 @@ open Libnames
 (** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
-val require_library_from_file : CUnix.physical_path -> bool option -> unit
 
 (** {6 Start the compilation of a library } *)
 
diff --git a/man/coqide.1 b/man/coqide.1
index cfd9c3b4a..6a3e67ad5 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -63,9 +63,11 @@ Load Coq file
 (Load Verbose
 .IR f .).
 .TP
-.BI \-load\-vernac\-object\  f
-Load Coq object file
-.IR f .vo.
+.BI \-load\-vernac\-object\  path
+Load Coq library
+.IR path
+(Require
+.IR path .).
 .TP
 .BI \-require\  path
 Load Coq library
diff --git a/man/coqtop.1 b/man/coqtop.1
index e079bee39..62d17aa67 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -73,9 +73,10 @@ load verbosely Coq file
 (Load Verbose filename.)
 
 .TP
-.BI \-load\-vernac\-object \ filename
-load Coq object file
-.I filename.vo
+.BI \-load\-vernac\-object \ path
+load Coq library
+.I path
+(Require path.)
 
 .TP
 .BI \-require \ path
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 32ac9a496..b7f1e4a19 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -171,8 +171,8 @@ let load_vernacular () =
 let load_vernacular_obj = ref ([] : string list)
 let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
 let load_vernac_obj () =
-  List.iter (fun f -> Library.require_library_from_file f None)
-    (List.rev !load_vernacular_obj)
+  let map dir = Qualid (Loc.ghost, qualid_of_string dir) in
+  Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj)
 
 let require_prelude () =
   let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in