aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-06-14 18:58:03 +0200
committerEmilio Jesus Gallego Arias2017-07-27 12:36:13 +0200
commit624dc13d0e80dcde22beecd3c80e68037899c287 (patch)
treecf614a1ac45fbf1a5800e242434135d944e2a84c /dev/doc
parent2a7ba998bf7d2c461fdbd8b710b7124395bafaa2 (diff)
[toplevel] Remove long ago deprecated and NOOP options.
Minor clean up, no sense in having these as they do nothing.
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