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/).

3 files changed, 10 insertions, 9 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
diff --git a/INSTALL.ide b/INSTALL.ide
index cb7ca325f..513e37c91 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -22,7 +22,7 @@ Else, read the rest of this document to compile your own CoqIde.
 
 COMPILATION REQUIREMENTS
 
-- OCaml >= 4.01 with native threads support.
+- OCaml >= 4.02.1 with native threads support.
 - make world must succeed.
 - The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
   The official supported version is at least 2.24.x.
diff --git a/configure.ml b/configure.ml
index 8a0d9afd0..d6552687c 100644
--- a/configure.ml
+++ b/configure.ml
@@ -487,14 +487,14 @@ let caml_version_nums =
          "Is it installed properly?")
 
 let check_caml_version () =
-  if caml_version_nums >= [4;2;3] then
+  if caml_version_nums >= [4;2;1] then
     printf "You have OCaml %s. Good!\n" caml_version
   else
     let () = printf "Your version of OCaml is %s.\n" caml_version in
     if !Prefs.force_caml_version then
       printf "*Warning* Your version of OCaml is outdated.\n"
     else
-      die "You need OCaml 4.02.3 or later."
+      die "You need OCaml 4.02.1 or later."
 
 let _ = check_caml_version ()