Revert "Merge remote-tracking branch 'github/pr/229' into trunk"

This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing
changes made to da99355b4d6de31aec5a660f7afe100190a8e683.

Hugo asked for more discussion on this topic, and it was not in the roadmap. I
merged it prematurely because I thought there was a consensus. Also, I missed
that it was changing coq_makefile. Sorry about that.

1 files changed, 10 insertions, 26 deletions

diff --git a/INSTALL b/INSTALL
index 56ff522dc..5a300010d 100644
--- a/INSTALL
+++ b/INSTALL
@@ -55,6 +55,8 @@ QUICK INSTALLATION PROCEDURE.
 1. ./configure
 2. make
 3. make install (you may need superuser rights)
+4. make clean
+
 
 INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 =================================================
@@ -130,13 +132,10 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 
 	make
 
-   to compile Coq in the best OCaml mode available (native-code if supported,
-   bytecode otherwise).
+   to compile Coq in Objective Caml bytecode (and native-code if supported).
 
    This will compile the entire system. This phase can take more or less time,
-   depending on your architecture and is fairly verbose. On a multi-core machine,
-   it is recommended to compile in parallel, via make -jN where N is your number
-   of cores.
+   depending on your architecture and is fairly verbose.
 
 6- You can now install the Coq system. Executables, libraries, manual pages
    and emacs mode are copied in some standard places of your system, defined at
@@ -152,19 +151,7 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
         (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
         (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t)
 
-7- Optionally, you could build the bytecode version of Coq via:
-
-        make byte
-
-   and install it via
-
-        make install-byte
-
-  This version is quite slower than the native code version of Coq, but could
-  be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml
-  toplevel accessible via the Drop command.
-
-8- You can now clean all the sources. (You can even erase them.)
+7- You can now clean all the sources. (You can even erase them.)
 
 	make clean
 
@@ -202,14 +189,11 @@ THE AVAILABLE COMMANDS.
 	coqtop		The Coq toplevel
 	coqc		The Coq compiler
 
-   Under architecture where ocamlopt is available, coqtop is the native code
-   version of Coq. On such architecture, you could additionally request
-   the build of the bytecode version of Coq via 'make byte' and install it via
-   'make install-byte'. This will create  an extra binary named coqtop.byte,
-   that could be used for debugging purpose. If native code isn't available,
-   coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte.
-   coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop
-   and coqc selects a particular binary.
+   Under architecture where ocamlopt is available, there are actually two
+   binaries for the interactive system, coqtop.byte and coqtop (respectively
+   bytecode and native code versions of Coq).  coqtop is a link to coqtop.byte
+   otherwise. coqc also invokes the fastest version of Coq.  Options -opt and
+   -byte to coqtop and coqc selects a particular binary.
 
     * `coqtop' launches Coq in the interactive mode. By default it loads
       basic logical definitions and tactics from the Init directory.