diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
| commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
| tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /dev/doc/debugging.txt | |
| parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
| parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) | |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'dev/doc/debugging.txt')
| -rw-r--r-- | dev/doc/debugging.txt | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index 50b3b45c..2480b8ed 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -11,6 +11,12 @@ 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();;' + You can avoid typing #use "include" (or "base_include") after Drop + by adding the following lines in your $HOME/.ocamlinit : + + if Filename.basename Sys.argv.(0) = "coqtop.byte" + then ignore (Toploop.use_silently Format.std_formatter "include") + Hints: To remove high-level pretty-printing features (coercions, notations, ...), use "Set Printing All". It will affect the #trace printers too. |