Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 11 insertions, 2 deletions

diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index e5c83139..50b3b45c 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -4,8 +4,8 @@ Debugging from Coq toplevel using Caml trace mechanism
   1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte)
   2. Access Ocaml toplevel using vernacular command 'Drop.'
   3. Install load paths and pretty printers for terms, idents, ... using
-     Ocaml command '#use "base_include";;' (use '#use "include";;' for a rawer
-     term pretty printer)
+     Ocaml command '#use "base_include";;' (use '#use "include";;' for 
+     installing the advanced term pretty printers)
   4. Use #trace to tell which function(s) to trace
   5. Go back to Coq toplevel with 'go();;'
   6. Test your Coq command and observe the result of tracing your functions
@@ -15,6 +15,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
 ============================