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

2 files changed, 19 insertions, 0 deletions

diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 50b3b45cc..2480b8edb 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 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: