diff options
| author | mdenes | 2013-01-22 14:18:38 +0000 |
|---|---|---|
| committer | mdenes | 2013-01-22 14:18:38 +0000 |
| commit | 62ce65dadb0afb8815b26069246832662846c7ec (patch) | |
| tree | 12d463433d64263510f3875b116f7b8cf16d43bc /dev/doc/patch.ocaml-3.10.drop.rectypes | |
| parent | e88df65bbc64b18da34a4233f680829025ca76d9 (diff) | |
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
Diffstat (limited to 'dev/doc/patch.ocaml-3.10.drop.rectypes')
| -rw-r--r-- | dev/doc/patch.ocaml-3.10.drop.rectypes | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/dev/doc/patch.ocaml-3.10.drop.rectypes b/dev/doc/patch.ocaml-3.10.drop.rectypes new file mode 100644 index 0000000000..ba7a3e9504 --- /dev/null +++ b/dev/doc/patch.ocaml-3.10.drop.rectypes @@ -0,0 +1,31 @@ +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 = |