Imported Upstream version 8.5~beta1+dfsg

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),