remove -rectypes except for term.ml

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

1 files changed, 2 insertions, 13 deletions

diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 60dfeb28d6..503d05883a 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -220,18 +220,7 @@ let tmp_dynlink()=
 let declare_loading_string () =
   if not !top then
     "Mltop.remove ();;"
-  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;;\
+  else "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));\
@@ -297,7 +286,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::"-rectypes"::args) in
+    let command = String.concat " " (prog::args) in
       if !echo then
 	begin
 	  print_endline command;