aboutsummaryrefslogtreecommitdiff
path: root/man
diff options
context:
space:
mode:
Diffstat (limited to 'man')
-rw-r--r--man/coqtop.118
1 files changed, 0 insertions, 18 deletions
diff --git a/man/coqtop.1 b/man/coqtop.1
index 084adfe453..addfb54672 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -85,22 +85,6 @@ load Coq library
and import it (Require Import path.)
.TP
-.BI \-compile \ filename.v
-compile Coq file
-.I filename.v
-(implies
-.B \-batch
-)
-
-.TP
-.BI \-compile\-verbose \ filename.v
-verbosely compile Coq file
-.I filename.v
-(implies
-.B \-batch
-)
-
-.TP
.B \-where
print Coq's standard library location and exit
@@ -125,8 +109,6 @@ batch mode (exits just after arguments parsing)
.B \-boot
boot mode (implies
.B \-q
-and
-.B \-batch
)
.TP