Relax required OCaml to 4.02.1.

We did not decide precisely what minor version we would support, so
relaxing. We document why 4.02.0 is not supported (its use is also
discouraged by the OCaml team, see e.g. https://ocaml.org/releases/).

1 files changed, 7 insertions, 6 deletions

diff --git a/INSTALL b/INSTALL
index df9e85527..9454bba4a 100644
--- a/INSTALL
+++ b/INSTALL
@@ -29,17 +29,18 @@ WHAT DO YOU NEED ?
 
    To compile Coq V8.6 yourself, you need:
 
-   - Objective Caml version 4.01.0 or later
+   - OCaml version 4.02.1 or later
      (available at http://caml.inria.fr/)
 
+     OCaml version 4.02.0 is not supported because of a severe performance
+     issue increasing compilation time.
+
    - Findlib (included in OCaml binary distribution under windows,
      probably available in your distribution and for sure at
      http://projects.camlcity.org/projects/findlib.html)
 
    - Camlp5 (version >= 6.02) (Coq compiles with Camlp4 but might be
-     less well supported, for instance, Objective Caml version 4.02.1
-     is then needed or a patched version of 4.01.0 as e.g. version
-     4.01.0-4 in Debian Jessie)
+     less well supported)
 
    - GNU Make version 3.81 or later
 
@@ -65,8 +66,8 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
    computer and that "ocamlc" (or, better, its native code version
    "ocamlc.opt") lies in a directory which is present in your $PATH
    environment variable. At the time of writing this sentence, all
-   versions of Objective Caml later or equal to 4.01.0 are
-   supported to the exception of Objective Caml 4.02.0.
+   versions of Objective Caml later or equal to 4.02.1 are
+   supported.
 
    To get Coq in native-code, (it runs 4 to 10 times faster than
    bytecode, but it takes more time to get compiled and the binary is