From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- tools/coqc.ml | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) (limited to 'tools/coqc.ml') 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 -- cgit v1.2.3