diff options
Diffstat (limited to 'man')
| -rw-r--r-- | man/coqdep.1 | 4 | ||||
| -rw-r--r-- | man/coqide.1 | 20 | ||||
| -rw-r--r-- | man/coqtop.1 | 29 |
3 files changed, 0 insertions, 53 deletions
diff --git a/man/coqdep.1 b/man/coqdep.1 index e9e0dd3e..5a6cd609 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -78,10 +78,6 @@ of each Coq file given as argument and complete (if needed) the list of Caml modules. The new command is printed on the standard output. No dependency is computed with this option. .TP -.BI \-slash -Prints paths using a slash instead of the OS specific separator. This -option is useful when developping under Cygwin. -.TP .BI \-I \ directory The files .v .ml .mli of the directory .IR directory \& diff --git a/man/coqide.1 b/man/coqide.1 index 9862ebb2..3fa7f0e4 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -40,17 +40,9 @@ to logical .B \-src Add source directories in the include path. .TP -.BI \-is\ f ,\ \-inputstate\ f -Read state from -.IR f .coq. -.TP .B \-nois Start with an empty state. .TP -.BI \-outputstate\ f -Write state in file -.IR f .coq. -.TP .BI \-load\-ml\-object\ f Load ML object file .IR f . @@ -93,12 +85,6 @@ Verbosely compile Coq file (implies .BR -batch ). .TP -.B \-opt -Run the native-code version of Coq or Coq_SearchIsos. -.TP -.B \-byte -Run the bytecode version of Coq or Coq_SearchIsos. -.TP .B \-where Print Coq's standard library location and exit. .TP @@ -135,12 +121,6 @@ Set sort Set impredicative. .TP .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 -.B COQ_XML_LIBRARY_ROOT -(if set) or to stdout (if unset). .SH SEE ALSO 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), |