Merge PR #967: Update debugging

2 files changed, 10 insertions, 9 deletions

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 84e60352ab..05f21895eb 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -22,7 +22,7 @@ If you want to minimize your bug (or help minimize someone else's) for more extr
 
 If you want to contribute a bug fix or feature yourself, pull requests on the [GitHub repository](https://github.com/coq/coq) are the way to contribute directly to the Coq implementation. We recommend you create a fork of the repository on GitHub and push your changes to a new "topic branch" in that fork. From there you can follow the [GitHub pull request documentation](https://help.github.com/articles/about-pull-requests/) to get your changes reviewed and pulled into the Coq source repository.
 
-Documentation for getting started with the Coq sources is located in various files in [`dev/doc`](/dev/doc) (for example, [debugging.txt](/dev/doc/debugging.txt)). For further help with the Coq sources, feel free to join the [Coq Gitter chat](https://gitter.im/coq/coq) and ask questions.
+Documentation for getting started with the Coq sources is located in various files in [`dev/doc`](/dev/doc) (for example, [debugging.md](/dev/doc/debugging.md)). For further help with the Coq sources, feel free to join the [Coq Gitter chat](https://gitter.im/coq/coq) and ask questions.
 
 Please make pull requests against the `master` branch.
 
diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.md
index 3e2b435b3e..b41206f3de 100644
--- a/dev/doc/debugging.txt
+++ 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
@@ -65,14 +66,14 @@ Global gprof-based profiling
 Per function profiling
 ======================
 
-   1. To profile function foo in file bar.ml, add the following lines, just
-      after the definition of the function:
+   To profile function foo in file bar.ml, add the following lines, just
+   after the definition of the function:
 
      let fookey = Profile.declare_profile "foo";;
      let foo a b c = Profile.profile3 fookey foo a b c;;
 
-     where foo is assumed to have three arguments (adapt using
-     Profile.profile1, Profile. profile2, etc).
+   where foo is assumed to have three arguments (adapt using
+   Profile.profile1, Profile. profile2, etc).
 
-     This has the effect to cumulate the time passed in foo under a
-     line of name "foo" which is displayed at the time coqtop exits.
+   This has the effect to cumulate the time passed in foo under a
+   line of name "foo" which is displayed at the time coqtop exits.