diff options
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) |