From 13db16609d4db3f174f718184cc36afb02e043ea Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 15 Oct 2011 14:28:54 +0000
Subject: 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
---
 dev/doc/debugging.txt | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dev/doc/debugging.txt')

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.
-- 
cgit v1.2.3