From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 man/coqchk.1 | 14 +++++++++++++-
 man/coqdep.1 |  5 +----
 man/coqdoc.1 |  4 ++++
 3 files changed, 18 insertions(+), 5 deletions(-)

(limited to 'man')

diff --git a/man/coqchk.1 b/man/coqchk.1
index b0a9c6ab..f51861f0 100644
--- a/man/coqchk.1
+++ b/man/coqchk.1
@@ -52,7 +52,7 @@ makes coqchk less verbose.
 .TP
 .BI \-admit \ file-or-module
 tag the specified module and all its dependencies as trusted, and will
-not be rechecked, unless explicitely requested by other options.
+not be rechecked, unless explicitly requested by other options.
 
 .TP
 .BI \-norec \ file-or-module
@@ -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),
diff --git a/man/coqdep.1 b/man/coqdep.1
index e2cbb40e..e9e0dd3e 100644
--- a/man/coqdep.1
+++ b/man/coqdep.1
@@ -39,7 +39,7 @@ When a directory is given as argument, it is recursively looked at.
 
 Dependencies of Coq modules are computed by looking at
 .IR Require \&
-commands (Require, Require Export, Require Import, Require Implementation),
+commands (Require, Require Export, Require Import),
 .IR Declare \& 
 .IR ML \& 
 .IR Module \&
@@ -69,9 +69,6 @@ is incorrect. (For instance, you wrote `Declare ML Module "A".',
 but the module A contains #open "B"). The correct command is printed
 (see option \-D). The warning is printed on standard error.
 .TP
-.BI \-i
-Prints also the dependencies for .vi files (Coq specification modules).
-.TP
 .BI \-D
 This commands looks for every command
 .IR Declare \& 
diff --git a/man/coqdoc.1 b/man/coqdoc.1
index e07ccdd3..8d71a874 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -120,6 +120,10 @@ globalizations are obtained with Coq option \-dump\-glob).
 .B \-\-no\-externals
 Do not insert links to the Coq standard library.
 
+.TP
+.BI \-\-external \ url \  libroot
+Set base URL for the external library whose root prefix is libroot.
+
 .TP
 .BI \-\-coqlib \ url
 Set base URL for the Coq standard library (default is http://coq.inria.fr/library/).
-- 
cgit v1.2.3