Fixing 50266aab on incompatibility of OCaml 4.01.0 with option -debug.

This was only when compiling with Camlp4 and it was producing an
assertion failure in asmcomp/emitaux.ml at line 226, reported as
OCaml's bug #6243.

Note: The issue of a problematic compilation with 4.01.0 was raised at
last WG.

1 files changed, 7 insertions, 3 deletions

diff --git a/configure.ml b/configure.ml
index 6291de03c..83005f0c5 100644
--- a/configure.ml
+++ b/configure.ml
@@ -520,9 +520,6 @@ let check_caml_version () =
       die ("Your version of OCaml is 4.02.0 which suffers from a bug inducing\n" ^
         "very slow compilation times. If you still want to use it, use \n" ^
         "option -force-caml-version.\n")
-    else if caml_version_nums = [4;1;0] && !Prefs.debug then
-      die ("Your version of OCaml is 4.01.0 which fails to compile Coq in " ^
-        "-debug mode.\nRemove -debug option or use a different version of OCaml.\n")
     else
       printf "You have OCaml %s. Good!\n" caml_version
   else
@@ -600,6 +597,12 @@ let check_camlp5_version () =
   | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n"
   | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
 
+let check_caml_version_for_camlp4 () =
+  if caml_version_nums = [4;1;0] && !Prefs.debug then
+    die ("Your version of OCaml is 4.01.0 which fails to compile Coq in -debug\n" ^
+            "mode with Camlp4. Remove -debug option or use a different version of OCaml\n" ^
+            "or use Camlp5.\n")
+
 let config_camlpX () =
   try
     if not !Prefs.usecamlp5 then raise NoCamlp5;
@@ -618,6 +621,7 @@ let config_camlpX () =
       let camlp4orf = which_camlpX "camlp4orf" in
       let version_line, _ = run ~err:StdOut camlp4orf ["-v"] in
       let camlp4_version = List.nth (string_split ' ' version_line) 2 in
+      check_caml_version_for_camlp4 ();
       "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod, camlp4_version
     with _ -> die "No Camlp4 installation found.\n"