diff options
| author | herbelin | 2009-02-17 00:14:05 +0000 |
|---|---|---|
| committer | herbelin | 2009-02-17 00:14:05 +0000 |
| commit | 0958c6e53dbfeec38cb774ab7479085acae56819 (patch) | |
| tree | 2c3afd8d615bff2970a718f22bfaf0ed622fc6f5 /dev | |
| parent | 77e22783cf3dac95ea9f122b84e011bf348c9893 (diff) | |
#rectypes was already automatically added when using 3.11
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11930 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/debugging.txt | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index 6e9f817f9e..50b3b45ccc 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -3,8 +3,6 @@ Debugging from Coq toplevel using Caml trace mechanism 1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte) 2. Access Ocaml toplevel using vernacular command 'Drop.' - 2.5 If with ocaml >= 3.11, use #rectypes to activate the option rectypes - in the toplevel 3. Install load paths and pretty printers for terms, idents, ... using Ocaml command '#use "base_include";;' (use '#use "include";;' for installing the advanced term pretty printers) |