diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-08-15 17:36:18 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-08-29 17:39:33 +0200 |
| commit | dd285233cff5eb67e4d394c6f7dabf40335ba33f (patch) | |
| tree | 7805c9ca74e61be1b6db40fae407f9eb6bfb8f7d /dev/doc | |
| parent | b14a346084d436b50a75858a395853fccb2207d0 (diff) | |
Adapt debugging doc to configure/Makefile changes.
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/debugging.md | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index 1c7b2bc97..b41206f3d 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 |