From 4dc07631599aaa342abebb6d78a3bcecd5d9dac6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Dec 2004 12:32:31 +0000
Subject: MAJ coq v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6496 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/debugging.txt | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/debugging.txt b/dev/debugging.txt
index 56cfe6463b..4c04c42fbe 100644
--- a/dev/debugging.txt
+++ b/dev/debugging.txt
@@ -12,10 +12,14 @@ Debugging from Coq toplevel using Caml trace mechanism
   6. Test your Coq command and observe the result of tracing your functions
   7. Freely switch from Coq to Ocaml toplevels with 'Drop.' and 'go();;'
 
+  Hints: To remove high-level pretty-printing features (coercions,
+  notations, ...), use "Set Printing All". It will affect the #trace
+  printers too.
+
 Debugging from Caml debugger
 ============================
 
-   Needs ocaml 3.06 (broken with ocaml 3.07 and 3.08)
+   Preferably use ocaml 3.06 (pretty-printing is broken with ocaml 3.07/3.08)
    Needs tuareg mode in Emacs
    Coq must be configured with -debug and -local (./configure -debug -local)
 
-- 
cgit v1.2.3