diff options
| author | letouzey | 2012-10-06 10:08:42 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-06 10:08:42 +0000 |
| commit | f975575187d0a19e7cc1afc43459a92eeb12b3f1 (patch) | |
| tree | 97d9c364c13ba82b6bfbafea40bbc5b040590c32 /dev/doc/debugging.txt | |
| parent | d2fd26a0ac600d066e79df4ab33b9bc924de069d (diff) | |
remove -rectypes except for term.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15871 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/doc/debugging.txt')
| -rw-r--r-- | dev/doc/debugging.txt | 9 |
1 files changed, 0 insertions, 9 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 ============================ |