The -require option now accepts a logical path instead of a physical one.

9 files changed, 28 insertions, 34 deletions

diff --git a/CHANGES b/CHANGES
index e3224db04..950f2fab1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -54,6 +54,8 @@ 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.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 2f9758fde..0f1823a02 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -157,10 +157,10 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
   Load \Coq~compiled file {\em file}{\tt .vo}
 
-\item[{\tt -require} {\em file}]\ 
+\item[{\tt -require} {\em path}]\ 
 
-  Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
-    Require} {\em file}).
+  Load \Coq~compiled library {\em path} and import it (equivalent to {\tt
+    Require Import} {\em path}).
 
 \item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ 
 
diff --git a/library/library.ml b/library/library.ml
index 1bcffcd14..a09f91b15 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -488,18 +488,8 @@ let rec_intern_library libs mref =
   let _, libs = intern_library libs mref None in
   libs
 
-let check_library_short_name f dir = function
-  | Some id when not (Id.equal id (snd (split_dirpath dir))) ->
-      errorlabstrm "check_library_short_name"
-      (str "The file " ++ str f ++ str " contains library" ++ spc () ++
-      pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
-      pr_id id)
-  | _ -> ()
-
-let rec_intern_by_filename_only id f =
+let rec_intern_by_filename_only f =
   let m = try intern_from_file f with Sys_error s -> error s in
-  (* Only the base name is expected to match *)
-  check_library_short_name f m.library_name id;
   (* We check no other file containing same library is loaded *)
   if library_is_loaded m.library_name then
     begin
@@ -518,12 +508,12 @@ let native_name_from_filename f =
   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 idopt f =
+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 idopt f
+  rec_intern_by_filename_only f
 
 (**********************************************************************)
 (*s [require_library] loads and possibly opens a library. This is a
@@ -600,8 +590,8 @@ let require_library_from_dirpath modrefl export =
       add_anonymous_leaf (in_require (needed,modrefl,export));
   add_frozen_state ()
 
-let require_library_from_file idopt file export =
-  let modref,needed = rec_intern_library_from_file idopt file in
+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));
diff --git a/library/library.mli b/library/library.mli
index f2e60718d..3d96f9a75 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -22,8 +22,7 @@ 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 :
-  Id.t option -> CUnix.physical_path -> 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 3fa7f0e41..cfd9c3b4a 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -67,11 +67,11 @@ Load Coq file
 Load Coq object file
 .IR f .vo.
 .TP
-.BI \-require\  f
-Load Coq object file
-.IR f .vo
-and import it (Require
-.IR f .).
+.BI \-require\  path
+Load Coq library
+.IR path
+and import it (Require Import
+.IR path .).
 .TP
 .BI \-compile\  f
 Compile Coq file
diff --git a/man/coqtop.1 b/man/coqtop.1
index 705ea43f6..e079bee39 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -78,10 +78,10 @@ load Coq object file
 .I filename.vo
 
 .TP
-.BI \-require \ filename
-load Coq object file
-.I filename.vo
-and import it (Require Import filename.)
+.BI \-require \ path
+load Coq library
+.I path
+and import it (Require Import path.)
 
 .TP
 .BI \-compile \ filename.v
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d67559d77..32ac9a496 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -171,7 +171,7 @@ 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 None f None)
+  List.iter (fun f -> Library.require_library_from_file f None)
     (List.rev !load_vernacular_obj)
 
 let require_prelude () =
@@ -185,9 +185,9 @@ let require_prelude () =
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
 let require () =
-  if !load_init then silently require_prelude ();
-  List.iter (fun s -> Library.require_library_from_file None s (Some false))
-    (List.rev !require_list)
+  let () = if !load_init then silently require_prelude () in
+  let map dir = Qualid (Loc.ghost, qualid_of_string dir) in
+  Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list)
 
 let compile_list = ref ([] : (bool * string) list)
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 3c001eadc..472503ced 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -42,7 +42,7 @@ let print_usage_channel co command =
 \n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose f.)\
 \n  -lv f	                 (idem)\
 \n  -load-vernac-object f  load Coq object file f.vo\
-\n  -require f             load Coq object file f.vo and import it (Require f.)\
+\n  -require path          load Coq library path and import it (Require Import path.)\
 \n  -compile f.v           compile Coq file f.v (implies -batch)\
 \n  -compile-verbose f.v   verbosely compile Coq file f.v (implies -batch)\
 \n  -quick                 quickly compile .v files to .vio files (skip proofs)\
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 4b1cd7a01..c6d87596d 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -16,6 +16,9 @@ val show_prooftree : unit -> unit
 
 val show_node : unit -> unit
 
+val vernac_require :
+  Libnames.reference option -> bool option -> Libnames.reference list -> unit
+
 (** This function can be used by any command that want to observe terms
    in the context of the current goal *)
 val get_current_context_of_args : int option -> Evd.evar_map * Environ.env