aboutsummaryrefslogtreecommitdiff
path: root/man
diff options
context:
space:
mode:
Diffstat (limited to 'man')
-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.)