aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/debugging.md
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc/debugging.md')
-rw-r--r--dev/doc/debugging.md5
1 files changed, 3 insertions, 2 deletions
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md
index 1c7b2bc974..b41206f3de 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -25,8 +25,9 @@ Debugging from Coq toplevel using Caml trace mechanism
Debugging from Caml debugger
============================
- Needs tuareg mode in Emacs
- Coq must be configured with -debug and -local (./configure -debug -local)
+ Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\
+ Coq must be configured with `-local` (`./configure -local`) and the
+ byte-code version of `coqtop` must have been generated with `make byte`.
1. M-x camldebug
2. give the binary name bin/coqtop.byte