diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-23 12:32:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-12-23 12:32:31 +0000 |
| commit | 4dc07631599aaa342abebb6d78a3bcecd5d9dac6 (patch) | |
| tree | d108dc65db284744e631e98a5d065eff74f49713 | |
| parent | af93a4a3640123e1a5acacaab0db9d9a8983613b (diff) | |
MAJ coq v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6496 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | dev/debugging.txt | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/dev/debugging.txt b/dev/debugging.txt index 56cfe6463..4c04c42fb 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) |