summaryrefslogtreecommitdiff
path: root/man/coqide.1
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:04:54 +0100
commit39efc41237ec906226a3a53d7396d51173495204 (patch)
tree87cd58d72d43469d2a2a0a127c1060d7c9e0206b /man/coqide.1
parent5fe4ac437bed43547b3695664974f492b55cb553 (diff)
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'man/coqide.1')
-rw-r--r--man/coqide.18
1 files changed, 2 insertions, 6 deletions
diff --git a/man/coqide.1 b/man/coqide.1
index 20379ef4..9862ebb2 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -12,11 +12,11 @@ coqide \- The Coq Proof Assistant graphical interface
.SH DESCRIPTION
-.B coqtop
+.B coqide
is a gtk graphical interface for the Coq proof assistant.
For command-line-oriented use of Coq, see
-.BR coqide (1)
+.BR coqtop (1)
; for batch-oriented use of Coq, see
.BR coqc (1).
@@ -112,10 +112,6 @@ Skip loading of rcfile.
Set the rcfile to
.IR f .
.TP
-.BI \-user\ u
-Use the rcfile of user
-.IR u .
-.TP
.B \-batch
Batch mode (exits just after arguments parsing).
.TP