Imported Upstream version 8.5~beta3+dfsg

1 files changed, 5 insertions, 10 deletions

diff --git a/tools/coqc.ml b/tools/coqc.ml
index 7e822dbe..e7239da6 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] *)
 
@@ -109,20 +104,20 @@ let parse_args () =
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
-      |"-impredicative-set"|"-vm"|"-no-native-compiler"
+      |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-verbose-compat-notations"|"-no-compat-notations"
-      |"-indices-matter"|"-quick"|"-color"|"-type-in-type"
+      |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
       as o) :: rem ->
 	parse (cfiles,o::args) rem
 
 (* Options for coqtop : b) options with 1 argument *)
 
-    | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
+    | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
-      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"
+      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
       as o) :: rem ->
 	begin
 	  match rem with