summaryrefslogtreecommitdiff
path: root/man/coqide.1
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /man/coqide.1
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
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