diff options
Diffstat (limited to 'dev/include')
| -rw-r--r-- | dev/include | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/dev/include b/dev/include index 705e8e375..13245eb5d 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: |