Revert "remove -rectypes except for term.ml"

Preparing landing of the native compiler, which requires -rectypes flag.

This reverts commit f975575187d0a19e7cc1afc43459a92eeb12b3f1.



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

1 files changed, 13 insertions, 2 deletions

diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 99fa8f6eba..6f05683ddd 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -221,7 +221,18 @@ let tmp_dynlink()=
 let declare_loading_string () =
   if not !top then
     "Mltop.remove ();;"
-  else "let ppf = Format.std_formatter;;\
+  else
+    "begin try\
+\n       (* Enable rectypes in the toplevel if it has the directive #rectypes *)\
+\n       begin match Hashtbl.find Toploop.directive_table \"rectypes\" with\
+\n         | Toploop.Directive_none f -> f ()\
+\n         | _ -> ()\
+\n       end\
+\n     with\
+\n       | Not_found -> ()\
+\n     end;;\
+\n\
+\n     let ppf = Format.std_formatter;;\
 \n     Mltop.set_top\
 \n       {Mltop.load_obj=\
 \n         (fun f -> if not (Topdirs.load_file ppf f) then Errors.error (\"Could not load plugin \"^f));\
@@ -288,7 +299,7 @@ let main () =
     (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
     let args = if !top then args @ [ "topstart.cmo" ] else args in
       (* Now, with the .cma, we MUST use the -linkall option *)
-    let command = String.concat " " (prog::args) in
+    let command = String.concat " " (prog::"-rectypes"::args) in
       if !echo then
 	begin
 	  print_endline command;