diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/debugging.txt | 6 | ||||
| -rw-r--r-- | dev/include | 13 |
2 files changed, 19 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. diff --git a/dev/include b/dev/include index 705e8e3754..13245eb5df 100644 --- a/dev/include +++ b/dev/include @@ -1,6 +1,19 @@ (* File to include to install the pretty-printers in the ocaml toplevel *) +(* Typical usage : + + $ coqtop.byte # or even better : rlwrap coqtop.byte + Coq < Drop. + # #use "include";; + + Alternatively, you can avoid typing #use "include" after each 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") +*) + (* For OCaml 3.10.x: clflags.cmi (a ocaml compilation by-product) must be in the library path. On Debian, install ocaml-compiler-libs, and uncomment the following: |