Set officially the minimal OCaml requirement to 3.12.1

 Anyway, a few syntactic features of 3.12 were already used here and
 there (e.g. local opening via Foo.(...), or the record shortcut
 { field; ... }). Hence compiling with 3.11 wasn't working anymore.

 Already take advantage of the following 3.12.1 features :
 - "module type of ..." in CArray, CList, CString ...
 - "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output
   via our coqdep to localize the .ml4 modules :-)

 The -ml-synonym option (+ various bugfixes) is the reason for asking
 3.12.1 directly and not just 3.12.0. After all, if debian stable is
 providing 3.12.1, then everybody has it ;-)

2 files changed, 0 insertions, 39 deletions

diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 2480b8edb..f0df2fc37 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -21,14 +21,6 @@ Debugging from Coq toplevel using Caml trace mechanism
   notations, ...), use "Set Printing All". It will affect the #trace
   printers too.
 
-Note for Ocaml 3.10.x: Ocaml 3.10.x requires that modules compiled
-with -rectypes are loaded in an environment with -rectypes set but
-there is no way to tell the toplevel to support -rectypes. To make it
-works, use "patch -p0 < dev/doc/patch.ocaml-3.10.drop.rectypes" to
-hack script/coqmktop.ml, then recompile coqtop.byte. The procedure
-above then works as soon as coqtop.byte is called with at least one
-argument (add neutral option -byte to ensure at least one argument).
-
 
 Debugging from Caml debugger
 ============================
diff --git a/dev/doc/patch.ocaml-3.10.drop.rectypes b/dev/doc/patch.ocaml-3.10.drop.rectypes
deleted file mode 100644
index ba7a3e950..000000000
--- a/dev/doc/patch.ocaml-3.10.drop.rectypes
+++ /dev/null
@@ -1,31 +0,0 @@
-Index: scripts/coqmktop.ml
-===================================================================
---- scripts/coqmktop.ml	(révision 12084)
-+++ scripts/coqmktop.ml	(copie de travail)
-@@ -231,12 +231,25 @@
-      end;;
- 
-      let ppf = Format.std_formatter;;
-+     let set_rectypes_hack () =
-+       if String.length (Sys.ocaml_version) >= 4 &
-+          String.sub (Sys.ocaml_version) 0 4 = \"3.10\"
-+       then
-+         (* ocaml 3.10 does not have #rectypes but needs it *)
-+         (* simulate a call with option -rectypes before *)
-+         (* jumping to the ocaml toplevel *)
-+         for i = 1 to Array.length Sys.argv - 1 do
-+           Sys.argv.(i) <- \"-rectypes\"
-+         done
-+       else
-+         () in
-+
-      Mltop.set_top
-        {Mltop.load_obj=
-          (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");
-         Mltop.use_file=Topdirs.dir_use ppf;
-         Mltop.add_dir=Topdirs.dir_directory;
--        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
-+        Mltop.ml_loop=(fun () -> set_rectypes_hack(); Topmain.main()) };;\n"
- 
- (* create a temporary main file to link *)
- let create_tmp_main_file modules =