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 ;-)

14 files changed, 18 insertions, 278 deletions

diff --git a/INSTALL b/INSTALL
index ca8d705c5..276c57601 100644
--- a/INSTALL
+++ b/INSTALL
@@ -41,7 +41,7 @@ WHAT DO YOU NEED ?
 
    Should you need or prefer to compile Coq V8.4 yourself, you need:
 
-     - Objective Caml version 3.11.2 or later
+     - Objective Caml version 3.12.1 or later
        (available at http://caml.inria.fr/)
 
      - Camlp5 (version <= 4.08, or 5.* transitional)
@@ -88,7 +88,7 @@ QUICK INSTALLATION PROCEDURE.
 INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
 =================================================
 
-1- Check that you have the Objective Caml compiler version 3.11.2 (or later)
+1- Check that you have the Objective Caml compiler version 3.12.1 (or later)
    installed on your computer and that "ocamlc" (or its native code version
    "ocamlc.opt") lie in a directory which is present in your $PATH environment
    variable.
diff --git a/INSTALL.ide b/INSTALL.ide
index b06fab1f6..2bbb4a5fc 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -23,7 +23,7 @@ On Gentoo GNU/Linux, do:
 Else, read the rest of this document to compile your own CoqIde.
 
 REQUIREMENT:
-	- OCaml >= 3.11.2 with native threads support.
+	- OCaml >= 3.12.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/Makefile.build b/Makefile.build
index f8895b2ed..7bfc6f953 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -106,7 +106,7 @@ OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS)
 
 BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
-DEPFLAGS= $(LOCALINCLUDES)
+DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils
 
 define bestocaml
 $(if $(OPT),\
@@ -928,10 +928,10 @@ endif
 	$(SHOW)'CAMLP4DEPS $<'
 	$(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(call CAMLP4DEPS,$<)" $(TOTARGET)
 
-# We now use coqdep_boot to wrap around ocamldep -modules, since it is aware
-# of .ml4 files
+# Since OCaml 3.12.1, we could use again ocamldep directly, thanks to
+# the option -ml-synonym
 
-OCAMLDEP_NG = $(COQDEPBOOT) -mldep $(OCAMLDEP)
+OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4
 
 checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
 	$(SHOW)'OCAMLDEP  $<'
diff --git a/configure.ml b/configure.ml
index 1c037269d..569e6ebd4 100644
--- a/configure.ml
+++ b/configure.ml
@@ -493,14 +493,14 @@ let caml_version_nums =
          "Is it installed properly?")
 
 let check_caml_version () =
-  if caml_version_nums >= [3;11;2] then
+  if caml_version_nums >= [3;12;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 3.11.2 or later."
+      die "You need OCaml 3.12.1 or later."
 
 let _ = check_caml_version ()
 
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 =
diff --git a/dev/include b/dev/include
index 9518034df..5eea5cc03 100644
--- a/dev/include
+++ b/dev/include
@@ -10,8 +10,9 @@
    Alternatively, you can avoid typing #use "include" after each Drop
    by adding the following lines in your $HOME/.ocamlinit :
 
+   #directory "+compiler-libs";;
    if Filename.basename Sys.argv.(0) = "coqtop.byte"
-   then ignore (Toploop.use_silently Format.std_formatter "include")
+   then ignore (Toploop.use_silently Format.std_formatter "dev/include")
 *)
 
 (* For OCaml 3.10.x:
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 77fb04322..ab3a4ba51 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -6,35 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-module type S =
-sig
-  external length : 'a array -> int = "%array_length"
-  external get : 'a array -> int -> 'a = "%array_safe_get"
-  external set : 'a array -> int -> 'a -> unit = "%array_safe_set"
-  external make : int -> 'a -> 'a array = "caml_make_vect"
-  val init : int -> (int -> 'a) -> 'a array
-  val make_matrix : int -> int -> 'a -> 'a array array
-  val create_matrix : int -> int -> 'a -> 'a array array
-  val append : 'a array -> 'a array -> 'a array
-  val concat : 'a array list -> 'a array
-  val sub : 'a array -> int -> int -> 'a array
-  val copy : 'a array -> 'a array
-  val fill : 'a array -> int -> int -> 'a -> unit
-  val blit : 'a array -> int -> 'a array -> int -> int -> unit
-  val to_list : 'a array -> 'a list
-  val of_list : 'a list -> 'a array
-  val iter : ('a -> unit) -> 'a array -> unit
-  val map : ('a -> 'b) -> 'a array -> 'b array
-  val iteri : (int -> 'a -> unit) -> 'a array -> unit
-  val mapi : (int -> 'a -> 'b) -> 'a array -> 'b array
-  val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
-  val fold_right : ('b -> 'a -> 'a) -> 'b array -> 'a -> 'a
-  val sort : ('a -> 'a -> int) -> 'a array -> unit
-  val stable_sort : ('a -> 'a -> int) -> 'a array -> unit
-  val fast_sort : ('a -> 'a -> int) -> 'a array -> unit
-  external unsafe_get : 'a array -> int -> 'a = "%array_unsafe_get"
-  external unsafe_set : 'a array -> int -> 'a -> unit = "%array_unsafe_set"
-end
+module type S = module type of Array
 
 module type ExtS =
 sig
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 83036e27c..e3a3bd7f5 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -6,37 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
-
-module type S =
-sig
-  external length : 'a array -> int = "%array_length"
-  external get : 'a array -> int -> 'a = "%array_safe_get"
-  external set : 'a array -> int -> 'a -> unit = "%array_safe_set"
-  external make : int -> 'a -> 'a array = "caml_make_vect"
-  val init : int -> (int -> 'a) -> 'a array
-  val make_matrix : int -> int -> 'a -> 'a array array
-  val create_matrix : int -> int -> 'a -> 'a array array
-  val append : 'a array -> 'a array -> 'a array
-  val concat : 'a array list -> 'a array
-  val sub : 'a array -> int -> int -> 'a array
-  val copy : 'a array -> 'a array
-  val fill : 'a array -> int -> int -> 'a -> unit
-  val blit : 'a array -> int -> 'a array -> int -> int -> unit
-  val to_list : 'a array -> 'a list
-  val of_list : 'a list -> 'a array
-  val iter : ('a -> unit) -> 'a array -> unit
-  val map : ('a -> 'b) -> 'a array -> 'b array
-  val iteri : (int -> 'a -> unit) -> 'a array -> unit
-  val mapi : (int -> 'a -> 'b) -> 'a array -> 'b array
-  val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
-  val fold_right : ('b -> 'a -> 'a) -> 'b array -> 'a -> 'a
-  val sort : ('a -> 'a -> int) -> 'a array -> unit
-  val stable_sort : ('a -> 'a -> int) -> 'a array -> unit
-  val fast_sort : ('a -> 'a -> int) -> 'a array -> unit
-  external unsafe_get : 'a array -> int -> 'a = "%array_unsafe_get"
-  external unsafe_set : 'a array -> int -> 'a -> unit = "%array_unsafe_set"
-end
+module type S = module type of Array
 
 module type ExtS =
 sig
diff --git a/lib/cList.ml b/lib/cList.ml
index 1a1993cd6..385c80b62 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -9,50 +9,7 @@
 type 'a cmp = 'a -> 'a -> int
 type 'a eq = 'a -> 'a -> bool
 
-module type S =
-sig
-  val length : 'a list -> int
-  val hd : 'a list -> 'a
-  val tl : 'a list -> 'a list
-  val nth : 'a list -> int -> 'a
-  val rev : 'a list -> 'a list
-  val append : 'a list -> 'a list -> 'a list
-  val rev_append : 'a list -> 'a list -> 'a list
-  val concat : 'a list list -> 'a list
-  val flatten : 'a list list -> 'a list
-  val iter : ('a -> unit) -> 'a list -> unit
-  val map : ('a -> 'b) -> 'a list -> 'b list
-  val rev_map : ('a -> 'b) -> 'a list -> 'b list
-  val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
-  val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
-  val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit
-  val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
-  val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
-  val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
-  val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
-  val for_all : ('a -> bool) -> 'a list -> bool
-  val exists : ('a -> bool) -> 'a list -> bool
-  val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
-  val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
-  val mem : 'a -> 'a list -> bool
-  val memq : 'a -> 'a list -> bool
-  val find : ('a -> bool) -> 'a list -> 'a
-  val filter : ('a -> bool) -> 'a list -> 'a list
-  val find_all : ('a -> bool) -> 'a list -> 'a list
-  val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
-  val assoc : 'a -> ('a * 'b) list -> 'b
-  val assq : 'a -> ('a * 'b) list -> 'b
-  val mem_assoc : 'a -> ('a * 'b) list -> bool
-  val mem_assq : 'a -> ('a * 'b) list -> bool
-  val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list
-  val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list
-  val split : ('a * 'b) list -> 'a list * 'b list
-  val combine : 'a list -> 'b list -> ('a * 'b) list
-  val sort : ('a -> 'a -> int) -> 'a list -> 'a list
-  val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list
-  val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list
-  val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
-end
+module type S = module type of List
 
 module type ExtS =
 sig
diff --git a/lib/cList.mli b/lib/cList.mli
index 6af32fdd0..15900260c 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -6,56 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
-
 type 'a cmp = 'a -> 'a -> int
 type 'a eq = 'a -> 'a -> bool
 
 (** Module type [S] is the one from OCaml Stdlib. *)
-module type S =
-sig
-  val length : 'a list -> int
-  val hd : 'a list -> 'a
-  val tl : 'a list -> 'a list
-  val nth : 'a list -> int -> 'a
-  val rev : 'a list -> 'a list
-  val append : 'a list -> 'a list -> 'a list
-  val rev_append : 'a list -> 'a list -> 'a list
-  val concat : 'a list list -> 'a list
-  val flatten : 'a list list -> 'a list
-  val iter : ('a -> unit) -> 'a list -> unit
-  val map : ('a -> 'b) -> 'a list -> 'b list
-  val rev_map : ('a -> 'b) -> 'a list -> 'b list
-  val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
-  val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
-  val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit
-  val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
-  val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
-  val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
-  val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
-  val for_all : ('a -> bool) -> 'a list -> bool
-  val exists : ('a -> bool) -> 'a list -> bool
-  val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
-  val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
-  val mem : 'a -> 'a list -> bool
-  val memq : 'a -> 'a list -> bool
-  val find : ('a -> bool) -> 'a list -> 'a
-  val filter : ('a -> bool) -> 'a list -> 'a list
-  val find_all : ('a -> bool) -> 'a list -> 'a list
-  val partition : ('a -> bool) -> 'a list -> 'a list * 'a list
-  val assoc : 'a -> ('a * 'b) list -> 'b
-  val assq : 'a -> ('a * 'b) list -> 'b
-  val mem_assoc : 'a -> ('a * 'b) list -> bool
-  val mem_assq : 'a -> ('a * 'b) list -> bool
-  val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list
-  val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list
-  val split : ('a * 'b) list -> 'a list * 'b list
-  val combine : 'a list -> 'b list -> ('a * 'b) list
-  val sort : ('a -> 'a -> int) -> 'a list -> 'a list
-  val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list
-  val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list
-  val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
-end
+module type S = module type of List
 
 module type ExtS =
 sig
diff --git a/lib/cString.ml b/lib/cString.ml
index 9be81bd3d..5c857077a 100644
--- a/lib/cString.ml
+++ b/lib/cString.ml
@@ -6,41 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** FIXME: use module type of *)
-module type S =
-sig
-  external length : string -> int = "%string_length"
-  external get : string -> int -> char = "%string_safe_get"
-  external set : string -> int -> char -> unit = "%string_safe_set"
-  external create : int -> string = "caml_create_string"
-  val make : int -> char -> string
-  val copy : string -> string
-  val sub : string -> int -> int -> string
-  val fill : string -> int -> int -> char -> unit
-  val blit : string -> int -> string -> int -> int -> unit
-  val concat : string -> string list -> string
-  val iter : (char -> unit) -> string -> unit
-  val escaped : string -> string
-  val index : string -> char -> int
-  val rindex : string -> char -> int
-  val index_from : string -> int -> char -> int
-  val rindex_from : string -> int -> char -> int
-  val contains : string -> char -> bool
-  val contains_from : string -> int -> char -> bool
-  val rcontains_from : string -> int -> char -> bool
-  val uppercase : string -> string
-  val lowercase : string -> string
-  val capitalize : string -> string
-  val uncapitalize : string -> string
-  type t = string
-  val compare: t -> t -> int
-  external unsafe_get : string -> int -> char = "%string_unsafe_get"
-  external unsafe_set : string -> int -> char -> unit = "%string_unsafe_set"
-  external unsafe_blit :
-    string -> int -> string -> int -> int -> unit = "caml_blit_string" "noalloc"
-  external unsafe_fill :
-    string -> int -> int -> char -> unit = "caml_fill_string" "noalloc"
-end
+module type S = module type of String
 
 module type ExtS =
 sig
diff --git a/lib/cString.mli b/lib/cString.mli
index 5f3616231..6aa10875c 100644
--- a/lib/cString.mli
+++ b/lib/cString.mli
@@ -6,43 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
-
 (** Module type [S] is the one from OCaml Stdlib. *)
-module type S =
-sig
-  external length : string -> int = "%string_length"
-  external get : string -> int -> char = "%string_safe_get"
-  external set : string -> int -> char -> unit = "%string_safe_set"
-  external create : int -> string = "caml_create_string"
-  val make : int -> char -> string
-  val copy : string -> string
-  val sub : string -> int -> int -> string
-  val fill : string -> int -> int -> char -> unit
-  val blit : string -> int -> string -> int -> int -> unit
-  val concat : string -> string list -> string
-  val iter : (char -> unit) -> string -> unit
-  val escaped : string -> string
-  val index : string -> char -> int
-  val rindex : string -> char -> int
-  val index_from : string -> int -> char -> int
-  val rindex_from : string -> int -> char -> int
-  val contains : string -> char -> bool
-  val contains_from : string -> int -> char -> bool
-  val rcontains_from : string -> int -> char -> bool
-  val uppercase : string -> string
-  val lowercase : string -> string
-  val capitalize : string -> string
-  val uncapitalize : string -> string
-  type t = string
-  val compare: t -> t -> int
-  external unsafe_get : string -> int -> char = "%string_unsafe_get"
-  external unsafe_set : string -> int -> char -> unit = "%string_unsafe_set"
-  external unsafe_blit :
-    string -> int -> string -> int -> int -> unit = "caml_blit_string" "noalloc"
-  external unsafe_fill :
-    string -> int -> int -> char -> unit = "caml_fill_string" "noalloc"
-end
+module type S = module type of String
 
 module type ExtS =
 sig
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 2c58a05e2..d8a30ee36 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -12,13 +12,6 @@
   open Printf
   open Lexing
 
-  (* A function that emulates Lexing.new_line (which does not exist in OCaml < 3.11.0) *)
-  let new_line lexbuf =
-    let pos = lexbuf.lex_curr_p in
-      lexbuf.lex_curr_p <- { pos with
-	pos_lnum = pos.pos_lnum + 1;
-	pos_bol = pos.pos_cnum }
-
   (* A list function we need *)
   let rec take n ls =
     if n = 0 then [] else
@@ -1065,7 +1058,7 @@ and body_bol = parse
   | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
 
 and body = parse
-  | nl {Tokens.flush_sublexer(); Output.line_break(); new_line lexbuf; body_bol lexbuf}
+  | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
   | nl+ space* "]]" space* nl
       { Tokens.flush_sublexer();
         if not !formatted then