Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 14 insertions, 34 deletions

diff --git a/INSTALL b/INSTALL
index 2b387b01..955e605c 100644
--- a/INSTALL
+++ b/INSTALL
@@ -6,19 +6,6 @@
 WHAT DO YOU NEED ?
 ==================
 
-   Coq is designed to work on computers equipped with a POSIX (Unix or a
-   clone) operating system. It also works under Microsoft Windows (see
-   INSTALL.win); for a MacOS X bundle application, see INSTALL.macosx.
-
-   Coq is known to be actively used under GNU/Linux (i386 and amd64) and
-   FreeBSD. Automated tests are run under many, many different architectures
-   under GNU/Linux.
-
-   Naturally, Coq will run faster on an architecture where OCaml can compile
-   to native code, rather than only bytecode.  See
-   http://caml.inria.fr/ocaml/portability.en.html for details.
-
-
    Your OS may already contain Coq under the form of a precompiled
    package or ready-to-compile port. In this case, and if the supplied
    version suits you, follow the usual procedure for your OS to
@@ -36,34 +23,31 @@ WHAT DO YOU NEED ?
 
      urpmi coq
 
-   - MacOS:
+   - MacPorts for MacOS X
 
      port install coq
 
-   Should you need or prefer to compile Coq V8.5 yourself, you need:
-
-     - Objective Caml version 3.12.1 or later
-       (available at http://caml.inria.fr/)
+   To compile Coq V8.5 yourself, you need:
 
-     - Camlp5 (version >= 6.06) (Coq compiles with Camlp4 but might be less
-       well supported)
+   - Objective Caml version 3.12.1 or later
+     (available at http://caml.inria.fr/)
 
-     - GNU Make version 3.81 or later
+   - Camlp5 (version >= 6.02) (Coq compiles with Camlp4 but might be less
+     well supported)
 
-     - a C compiler
+   - GNU Make version 3.81 or later
 
-     - for Coqide, the Lablgtk development files, and the GTK libraries
-       incuding gtksourceview, see INSTALL.ide for more details
+   - a C compiler
 
-   By FTP, Coq comes as a single compressed tar-file. You have
-   probably already decompressed it if you are reading this document.
+   - for Coqide, the Lablgtk development files, and the GTK libraries
+     incuding gtksourceview, see INSTALL.ide for more details
 
 
 QUICK INSTALLATION PROCEDURE.
 =============================
 
 1. ./configure
-2. make world
+2. make
 3. make install (you may need superuser rights)
 4. make clean
 
@@ -132,17 +116,13 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
         Compile Coq to run in its source directory. The installation (step 6)
         is not necessary in that case.
 
--opt
-        Use the ocamlc.opt compiler instead of ocamlc (and ocamlopt.opt
-        compiler instead of ocamlopt). Makes compilation faster (recommended).
-
 -browser <command>
 	Use <command> to open an URL in a browser. %s must appear in <command>,
 	and will be replaced by the URL.
 
 5- Still in the root directory, do
 
-	make world
+	make
 
    to compile Coq in Objective Caml bytecode (and native-code if supported).
 
@@ -219,7 +199,7 @@ THE AVAILABLE COMMANDS.
       command "Require".
 
    A detailed description of these commands and of their options is given
-   in the Reference Manual (which you can get by FTP, in the doc/
+   in the Reference Manual (which you can get in the doc/
    directory, or read online on http://coq.inria.fr/doc/)
    and in the corresponding manual pages.
 
@@ -291,7 +271,7 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
        during compilation of binary packages);
      - install dllcoqrun.so in a location listed in the file ld.conf that is in
        the directory of the standard library of OCaml;
-     - recompile your bytecode executables after reconfiguring the location of
+     - recompile your bytecode executables after reconfiguring the location
        of the shared library:
          ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
        where <path> is the directory where the dllcoqrun.so is installed;