Execute #rectypes directive in embedded OCaml toplevel...

...to avoid the need to have cflags.cmi around. This directive will
likely be available in the next version of OCaml. See OCaml bug #4460.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11605 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 14 insertions, 4 deletions

diff --git a/dev/include b/dev/include
index ccb75edd5a..364773753d 100644
--- a/dev/include
+++ b/dev/include
@@ -1,12 +1,13 @@
 
 (* File to include to install the pretty-printers in the ocaml toplevel *)
 
-(* clflags.cmi (a ocaml compilation by-product) must be in the library path.
+(* For OCaml 3.10.x:
+   clflags.cmi (a ocaml compilation by-product) must be in the library path.
    On Debian, install ocaml-compiler-libs, and uncomment the following:
    #directory "+compiler-libs/utils";;
+   Clflags.recursive_types := true;;
 *)
 
-(* Clflags.recursive_types := true;;*)
 #cd ".";;
 #use "base_include";;
 
@@ -37,4 +38,3 @@
 #install_printer  (* generic_argument *) pp_generic_argument;;
 
 #install_printer  (* fconstr *) ppfconstr;;
-
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 320cbe1824..1b9247616d 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -210,7 +210,17 @@ let declare_loading_string () =
   if not !top then
     "Mltop.remove ();;"
   else
-    "let ppf = Format.std_formatter;;
+    "begin try
+       (* Enable rectypes in the toplevel if it has the directive #rectypes *)
+       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with
+         | Toploop.Directive_none f -> f ()
+         | _ -> ()
+       end
+     with
+       | Not_found -> ()
+     end;;
+
+     let ppf = Format.std_formatter;;
      Mltop.set_top
        {Mltop.load_obj=Topdirs.dir_load ppf;
         Mltop.use_file=Topdirs.dir_use ppf;