diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-24 18:45:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-25 11:19:08 +0200 |
| commit | b6725a2d0077239e51385a62a526ab9465eea26d (patch) | |
| tree | 7af2a0e3fe9b3a4c40b1e46de9e1211ec0e859cb /toplevel/vernac.ml | |
| parent | 2ba2ca96be88bad5cd75a02c94cc48ef4f5209b7 (diff) | |
The -compile option now accepts ".v" files and outputs a warning otherwise.
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 266d8f9b4..14d2bcea4 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -294,7 +294,15 @@ let load_vernac verb file = if !Flags.beautify_file then close_out !chan_beautify; raise_with_file file (disable_drop e, info) -(* Compile a vernac file (f is assumed without .v suffix) *) +let ensure_v f = + if Filename.check_suffix f ".v" then f + else begin + msg_warning (str "File \"" ++ str f ++ strbrk "\" has been implicitly \ + expanded to \"" ++ str f ++ str ".v\""); + f ^ ".v" + end + +(* Compile a vernac file *) let compile verbosely f = let check_pending_proofs () = let pfs = Pfedit.get_all_proof_names () in @@ -302,7 +310,8 @@ let compile verbosely f = (msg_error (str "There are pending proofs"); flush_all (); exit 1) in match !Flags.compilation_mode with | BuildVo -> - let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in + let long_f_dot_v = ensure_v f in + let ldir = Flags.verbosely Library.start_library long_f_dot_v in Stm.set_compilation_hints long_f_dot_v; Aux_file.start_aux_file_for long_f_dot_v; Dumpglob.start_dump_glob long_f_dot_v; @@ -318,7 +327,8 @@ let compile verbosely f = Aux_file.stop_aux_file (); Dumpglob.end_dump_glob () | BuildVio -> - let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in + let long_f_dot_v = ensure_v f in + let ldir = Flags.verbosely Library.start_library long_f_dot_v in Dumpglob.noglob (); Stm.set_compilation_hints long_f_dot_v; let _ = load_vernac verbosely long_f_dot_v in |