From 84b3ae516fffffc60989817eab9cf5749c2f492a Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 1 Dec 2009 21:49:23 +0000
Subject: fix coqchk options documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12552 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/checker.ml |  5 +++--
 man/coqchk.1       | 12 ++++++++++++
 2 files changed, 15 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
 
diff --git a/man/coqchk.1 b/man/coqchk.1
index b0a9c6abf..2709a4be4 100644
--- a/man/coqchk.1
+++ b/man/coqchk.1
@@ -73,6 +73,18 @@ verified: assumptions and usage of impredicativity
 allows the checker to verify libraries that have been compiled with
 this flag.
 
+.TP
+.BI \-v
+print Coq version and exit
+
+.TP
+.BI \-where
+print Coq's standard library location and exit
+
+.TP
+.BI \-h,\ \-\-help
+print list of options
+
 .SH SEE ALSO
 
 .BR coqtop (1),
-- 
cgit v1.2.3