aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-01-29 22:40:58 +0100
committerPierre-Marie Pédrot2015-01-29 22:40:58 +0100
commita340265c9f88df990649481c8ecbe8a513ac4756 (patch)
treec9e02defb10bcdb258d75cb6f156657654f65f1f /tools
parent51b15993cb4a9cc2521b6107b7f4195b21040087 (diff)
parentdb293d185f8deb091d4b086f327caa0f376d67d7 (diff)
Merge branch 'v8.5'
Diffstat (limited to 'tools')
-rw-r--r--tools/coqc.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml
index f636ffd87a..5c7be41bec 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -111,7 +111,7 @@ let parse_args () =
|"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
|"-impredicative-set"|"-vm"|"-no-native-compiler"
|"-verbose-compat-notations"|"-no-compat-notations"
- |"-indices-matter"|"-quick"|"-color"
+ |"-indices-matter"|"-quick"|"-color"|"-type-in-type"
|"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
as o) :: rem ->
parse (cfiles,o::args) rem