remove -rectypes except for term.ml

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

2 files changed, 0 insertions, 40 deletions

diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 2480b8edb3..83512c658b 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -21,15 +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 ba7a3e9504..0000000000
--- 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 =