Updating the documentation and the toolchain w.r.t. the change in -compile.

7 files changed, 15 insertions, 17 deletions

diff --git a/CHANGES b/CHANGES
index c8fca217f..e3224db04 100644
--- a/CHANGES
+++ b/CHANGES
@@ -51,6 +51,9 @@ Tools
 - Flag -no-native-compiler was removed and became the default for coqc. If
   precompilation of files for native conversion test is desired, use
   -native-compiler.
+- 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.
 
 Changes from V8.5beta1 to V8.5beta2
 ===================================
diff --git a/Makefile.build b/Makefile.build
index 6ceff2de9..39f60bd59 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -587,7 +587,7 @@ pluginsbyte: $(PLUGINS)
 theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
 	$(SHOW)'COQC -noinit $<'
 	$(HIDE)rm -f theories/Init/$*.glob
-	$(HIDE)$(BOOTCOQC) theories/Init/$* -noinit -R theories Coq
+	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq
 
 theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml
 	$(OCAML) $< $(TOTARGET)
@@ -1038,7 +1038,7 @@ plugins/%_mod.ml: plugins/%.mllib
 %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
 	$(SHOW)'COQC      $<'
 	$(HIDE)rm -f $*.glob 
-	$(HIDE)$(BOOTCOQC) $*
+	$(HIDE)$(BOOTCOQC) $<
 ifdef VALIDATE
 	$(SHOW)'COQCHK    $(call vo_to_mod,$@)'
 	$(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 6335dfd32..2f9758fde 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -162,11 +162,11 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
   Load \Coq~compiled file {\em file}{\tt .vo} and import it ({\tt
     Require} {\em file}).
 
-\item[{\tt -compile} {\em file},{\tt -compile-verbose} {\em file}, {\tt -batch}]\ 
+\item[{\tt -compile} {\em file.v},{\tt -compile-verbose} {\em file.v}, {\tt -batch}]\ 
 
   {\tt coqtop} options only used internally by {\tt coqc}.
 
-  This compiles file {\em file}{\tt .v} into {\em file}{\tt .vo} without/with a
+  This compiles file {\em file.v} into {\em file}{\tt .vo} without/with a
   copy of the contents of the file on standard input.  This option implies options
   {\tt -batch} (exit just after arguments parsing). It is only
   available for {\tt coqtop}.
diff --git a/man/coqtop.1 b/man/coqtop.1
index 1bc4629d0..705ea43f6 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -84,7 +84,7 @@ load Coq object file
 and import it (Require Import filename.)
 
 .TP
-.BI \-compile \ filename
+.BI \-compile \ filename.v
 compile Coq file
 .I filename.v 
 (implies 
@@ -92,7 +92,7 @@ compile Coq file
 )
 
 .TP
-.BI \-compile\-verbose \ filename
+.BI \-compile\-verbose \ filename.v
 verbosely compile Coq file
 .I filename.v
 (implies 
diff --git a/test-suite/Makefile b/test-suite/Makefile
index d2466250a..39c36d541 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -208,7 +208,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) "$*" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \
 	  if [ $$R != 0 ]; then \
 	    echo $(log_failure); \
 	    echo "    $<...could not be prepared" ; \
@@ -238,7 +238,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  $(coqc) "$*" $(call get_coq_prog_args,"$<") -async-proofs on \
+	  $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \
 	    -async-proofs-private-flags fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \
 	    $$opts 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
@@ -352,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
 # Additionnal dependencies for module tests
 $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo
 modules/%.vo: modules/%.v
-	$(HIDE)$(coqtop) -R modules Mods -compile $(<:.v=)
+	$(HIDE)$(coqtop) -R modules Mods -compile $<
 
 #######################################################################
 # Miscellaneous tests
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5710b97f2..e7239da68 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -30,13 +30,8 @@ let verbose = ref false
 let rec make_compilation_args = function
   | [] -> []
   | file :: fl ->
-      let file_noext =
-        if Filename.check_suffix file ".v" then
-          Filename.chop_suffix file ".v"
-        else file
-      in
       (if !verbose then "-compile-verbose" else "-compile")
-      :: file_noext :: (make_compilation_args fl)
+      :: file :: (make_compilation_args fl)
 
 (* compilation of files [files] with command [command] and args [args] *)
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index a5d8450b9..3c001eadc 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -43,8 +43,8 @@ let print_usage_channel co command =
 \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  -compile f             compile Coq file f.v (implies -batch)\
-\n  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)\
+\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)\
 \n  -schedule-vio2vo j f1..fn   run up to j instances of Coq to turn each fi.vio\
 \n                         into fi.vo\