The -compile option now accepts ".v" files and outputs a warning otherwise.

2 files changed, 12 insertions, 10 deletions

diff --git a/library/library.ml b/library/library.ml
index f7ca4e976..1bcffcd14 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -678,22 +678,22 @@ let check_module_name s =
     | c -> err c
 
 let start_library f =
-  let paths = Loadpath.get_paths () in
-  let _, longf =
-    System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+  let () = if not (Sys.file_exists f) then
+    errorlabstrm "" (hov 0 (str "Can't find file" ++ spc () ++ str f))
+  in
   let ldir0 =
     try
-      let lp = Loadpath.find_load_path (Filename.dirname longf) in
+      let lp = Loadpath.find_load_path (Filename.dirname f) in
       Loadpath.logical lp
     with Not_found -> Nameops.default_root_prefix
   in
-  let file = Filename.basename f in
+  let file = Filename.chop_extension (Filename.basename f) in
   let id = Id.of_string file in
   check_module_name file;
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
   Declaremods.start_library ldir;
-  ldir,longf
+  ldir
 
 let load_library_todo f =
   let paths = Loadpath.get_paths () in
diff --git a/library/library.mli b/library/library.mli
index 967a54e4c..f2e60718d 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -25,7 +25,7 @@ val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> u
 val require_library_from_file :
   Id.t option -> CUnix.physical_path -> bool option -> unit
 
-(** {6 ... } *)
+(** {6 Start the compilation of a library } *)
 
 (** Segments of a library *)
 type seg_sum
@@ -39,10 +39,12 @@ type seg_proofs = Term.constr Future.computation array
    an export otherwise just a simple import *)
 val import_module : bool -> qualid located list -> unit
 
-(** {6 Start the compilation of a library } *)
-val start_library : string -> DirPath.t * string
+(** Start the compilation of a file as a library. The argument must be an
+    existing file on the system, and the returned path is the associated
+    absolute logical path of the library. *)
+val start_library : CUnix.physical_path -> DirPath.t
 
-(** {6 End the compilation of a library and save it to a ".vo" file } *)
+(** End the compilation of a library and save it to a ".vo" file *)
 val save_library_to :
   ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) ->
   DirPath.t -> string -> Opaqueproof.opaquetab -> unit