diff options
Diffstat (limited to 'man/coqtop.1')
| -rw-r--r-- | man/coqtop.1 | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/man/coqtop.1 b/man/coqtop.1 index fff813bb..1bc4629d 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -47,20 +47,10 @@ set the toplevel name to be instead of Top .TP -.BI \-inputstate \ filename, \ \-is \ filename -read state from file -.I filename.coq - -.TP .B \-nois start with an empty initial state .TP -.BI \-outputstate filename -write state in file -.I filename.coq - -.TP .BI \-load\-ml\-object \ filename load ML object file .I filenname @@ -110,14 +100,6 @@ verbosely compile Coq file ) .TP -.B \-opt -run the native\-code version of Coq - -.TP -.B \-byte -run the bytecode version of Coq - -.TP .B \-where print Coq's standard library location and exit @@ -170,17 +152,6 @@ set sort Set impredicative .B \-dont\-load\-proofs don't load opaque proofs in memory -.TP -.B \-xml -export XML files either to the hierarchy rooted in -the directory $COQ_XML_LIBRARY_ROOT (if set) or to -stdout (if unset) - -.TP -.B \-quality -improve the legibility of the proof terms produced by -some tactics - .SH SEE ALSO .BR coqc (1), |