summaryrefslogtreecommitdiff
path: root/man/coqc.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/coqc.1
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'man/coqc.1')
-rw-r--r--man/coqc.112
1 files changed, 12 insertions, 0 deletions
diff --git a/man/coqc.1 b/man/coqc.1
index 7113d504..1e597afd 100644
--- a/man/coqc.1
+++ b/man/coqc.1
@@ -40,6 +40,18 @@ with option
it accepts the same options as
.B coqtop.
+.TP
+.BI \-image \ bin
+use
+.I bin
+as underlying
+.B coqtop
+instead of the default one.
+
+.TP
+.BI \-verbose
+print the compiled file on the standard output.
+
.SH SEE ALSO
.BR coqtop (1),