diff options
| author | letouzey | 2011-10-15 14:28:54 +0000 |
|---|---|---|
| committer | letouzey | 2011-10-15 14:28:54 +0000 |
| commit | 13db16609d4db3f174f718184cc36afb02e043ea (patch) | |
| tree | adb515fd063fbd80fe19219fd49a0391a1a7d567 /dev/doc | |
| parent | 25ba10c14d8771367fbda6efe8174e10769aa739 (diff) | |
debugging.txt: no more typing of #use "include" if using .ocamlinit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14562 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/doc')
| -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 50b3b45ccc..2480b8edb3 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. |