diff options
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coqc.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml index e835091ea..d7f1bebdf 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -120,7 +120,7 @@ let parse_args () = |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" |"-impredicative-set"|"-vm"|"-no-native-compiler" |"-verbose-compat-notations"|"-no-compat-notations" - |"-quick" + |"-indices-matter"|"-quick" as o) :: rem -> parse (cfiles,o::args) rem @@ -158,8 +158,6 @@ let parse_args () = extra_arg_needed := false; parse (cfiles, List.rev nodash @ s :: o :: args) rem -(* Anything else is interpreted as a file *) - | f :: rem -> if Sys.file_exists f then parse (f::cfiles,args) rem |