aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqc.ml
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-06-12 20:00:18 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-06-30 15:55:55 +0200
commita82eb26100d55110ce7d7cb508d49d1fad8ebd37 (patch)
tree83445ee708c64a7b51a4e1d021793f7ba4ebe2d4 /tools/coqc.ml
parente1d46f1c6ca9556e23e5378c6589220fc48da879 (diff)
coqc is -Q aware
Diffstat (limited to 'tools/coqc.ml')
-rw-r--r--tools/coqc.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 90585c763..1d416a1c4 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -126,6 +126,7 @@ let parse_args () =
| "-R" :: s :: "-as" :: t :: rem -> parse (cfiles,t::"-as"::s::"-R"::args) rem
| "-R" :: s :: "-as" :: [] -> usage ()
| "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
+ | "-Q" :: s :: t :: rem -> parse (cfiles,t::s::"-Q"::args) rem
| ("-schedule-vi-checking"
|"-check-vi-tasks" | "-schedule-vi2vo" as o) :: s :: rem ->
let nodash, rem =