Remove documentation for the unsupported options -byte and -opt.

5 files changed, 7 insertions, 27 deletions

diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 172af9730..20088fd72 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -24,10 +24,9 @@ run by the command {\tt coqtop}.
 \label{binary-images}
 They are two different binary images of \Coq: the byte-code one and
 the native-code one (if Objective Caml provides a native-code compiler
-for your platform, which is supposed in the following).  When invoking
-\verb!coqtop! or \verb!coqc!, the native-code version of the system is
-used.  The command-line options \verb!-byte! and \verb!-opt! explicitly
-select the byte-code and the native-code versions, respectively.
+for your platform, which is supposed in the following). By default,
+\verb!coqc! executes the native-code version; this can be overridden
+using the \verb!-byte! option.
 
 The byte-code toplevel is based on a Caml
 toplevel (to allow the dynamic link of tactics).  You can switch to
@@ -43,11 +42,7 @@ compile it into a {\em file}{\tt .vo} file (See ~\ref{compiled}).
 defined in the Section~\ref{lexical}. It
 must only contain letters, digits or underscores
 (\_). Thus it can be \verb+/bar/foo/toto.v+ but cannot be
-\verb+/bar/foo/to-to.v+ . 
-
-Notice that the \verb!-byte! and \verb!-opt! options are still
-available with \verb!coqc!  and allow you to select the byte-code or
-native-code versions of the system.
+\verb+/bar/foo/to-to.v+.
 
 \section[Customization]{Customization at launch time}
 
diff --git a/man/coqide.1 b/man/coqide.1
index 9862ebb25..013c2ed7f 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -93,12 +93,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
diff --git a/man/coqtop.1 b/man/coqtop.1
index fff813bb0..8006d4993 100644
--- a/man/coqtop.1
+++ b/man/coqtop.1
@@ -110,14 +110,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
 
diff --git a/tools/coqc.ml b/tools/coqc.ml
index d7f1bebdf..0a9ea4e89 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -82,7 +82,7 @@ let parse_args () =
     | "-image" :: f :: rem -> image := f; parse (cfiles,args) rem
     | "-image" :: [] ->	usage ()
     | "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem
-    | "-opt" :: rem -> (* now a no-op *) parse (cfiles,args) rem
+    | "-opt" :: rem -> binary := "coqtop"; parse (cfiles,args) rem
 
 (* Obsolete options *)
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e8e0292bc..19dbfef19 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -48,9 +48,6 @@ let print_usage_channel co command =
 \n  -compile f             compile Coq file f.v (implies -batch)\
 \n  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)\
 \n\
-\n  -opt                   run the native-code version of Coq\
-\n  -byte                  run the bytecode version of Coq\
-\n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config                print Coq's configuration information and exit\
 \n  -v                     print Coq version and exit\
@@ -89,6 +86,8 @@ let print_usage_coqc () =
 \noptions are:\
 \n  -verbose  compile verbosely\
 \n  -image f  specify an alternative executable for Coq\
+\n  -opt      run the native-code version of Coq\
+\n  -byte     run the bytecode version of Coq\
 \n  -t        keep temporary files\n\n"
 
 (* Print the configuration information *)