summaryrefslogtreecommitdiff
path: root/man/coqide.1
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:43:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:43:34 +0100
commit4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch)
treeaefad2e3de35f75c46729f9310d33b56d3821961 /man/coqide.1
parent64fa31c7ee53e79b112507fb2eea27dc7648328d (diff)
parent91dbeab8eef959c3f64960909ca69d4e68c8198d (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'man/coqide.1')
-rw-r--r--man/coqide.120
1 files changed, 11 insertions, 9 deletions
diff --git a/man/coqide.1 b/man/coqide.1
index 3fa7f0e4..6a3e67ad 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -63,15 +63,17 @@ Load Coq file
(Load Verbose
.IR f .).
.TP
-.BI \-load\-vernac\-object\ f
-Load Coq object file
-.IR f .vo.
-.TP
-.BI \-require\ f
-Load Coq object file
-.IR f .vo
-and import it (Require
-.IR f .).
+.BI \-load\-vernac\-object\ path
+Load Coq library
+.IR path
+(Require
+.IR path .).
+.TP
+.BI \-require\ path
+Load Coq library
+.IR path
+and import it (Require Import
+.IR path .).
.TP
.BI \-compile\ f
Compile Coq file