aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
authorMaxime Dénès2017-08-01 13:00:53 +0200
committerMaxime Dénès2017-08-01 13:00:53 +0200
commit82df5a27656753f50b5f5ff7d1faa37b2ddefc49 (patch)
tree50698225f72a6e7cc09838ad245b7effde5d735c /dev/doc
parent2f349829c125ed0e2d55548935e7b90e7719f12e (diff)
parent624dc13d0e80dcde22beecd3c80e68037899c287 (diff)
Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.
Diffstat (limited to 'dev/doc')
-rw-r--r--dev/doc/debugging.txt2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt
index 79cde48849..3e2b435b3e 100644
--- a/dev/doc/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -1,7 +1,7 @@
Debugging from Coq toplevel using Caml trace mechanism
======================================================
- 1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte)
+ 1. Launch bytecode version of Coq (coqtop.byte)
2. Access Ocaml toplevel using vernacular command 'Drop.'
3. Install load paths and pretty printers for terms, idents, ... using
Ocaml command '#use "base_include";;' (use '#use "include";;' for