aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2020-04-02 15:51:09 +0200
committerThéo Zimmermann2020-04-02 22:14:01 +0200
commit0c1382bd0a9c41b559a912695e2154b758de7b18 (patch)
tree6a2749527fd05e837bceb3e5435be0328572e116
parentefa833d06990262174195fdc43a542d272b480a3 (diff)
Minimal fix to man pages.
-rw-r--r--man/coqide.12
-rw-r--r--man/coqtop.12
2 files changed, 2 insertions, 2 deletions
diff --git a/man/coqide.1 b/man/coqide.1
index 62a102af03..c1af046019 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -69,7 +69,7 @@ Load Coq library
(Require
.IR path .).
.TP
-.BI \-require\ path
+.BI \-require-import\ path
Load Coq library
.IR path
and import it (Require Import
diff --git a/man/coqtop.1 b/man/coqtop.1
index 25d0ef7718..e799bc7748 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -79,7 +79,7 @@ load Coq library
(Require path.)
.TP
-.BI \-require \ path
+.BI \-require-import \ path
load Coq library
.I path
and import it (Require Import path.)