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/debugging.txt | |
| 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/debugging.txt')
| -rw-r--r-- | dev/doc/debugging.txt | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index 83512c658b..2480b8edb3 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -21,6 +21,15 @@ 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 ============================ |