aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/checker.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/checker.ml')
-rw-r--r--checker/checker.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index 1df187328..712566a00 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -182,8 +182,9 @@ let print_usage_channel co command =
-where print Coq's standard library location and exit
-v print Coq version and exit
-boot boot mode
- -o print the list of assumptions
- -m print the maximum heap size
+ -o, --output-context print the list of assumptions
+ -m, --memoty print the maximum heap size
+ -silent disable trace of constants being checked
-impredicative-set set sort Set impredicative