diff options
| author | Maxime Dénès | 2017-04-14 13:56:56 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-14 13:56:56 +0200 |
| commit | fd197553c11bc968aa13b9db6a49608b5d8accc4 (patch) | |
| tree | 0e41cd7b9c4a16a1cba79ddce4581da04953668a | |
| parent | 81993897584b2f6bf9e6575eee44bd09a7b79f0e (diff) | |
| parent | c50f62734c6d180561c6a65679daef591d565944 (diff) | |
Merge PR#554: Update INSTALL now that -debug is the default.
| -rw-r--r-- | INSTALL | 14 |
1 files changed, 4 insertions, 10 deletions
@@ -168,16 +168,10 @@ INSTALLATION PROCEDURE FOR ADVANCED USERS. Then compile the sources as described in step 5 above. The resulting binaries will reside in the subdirectory bin/. - If you want to compile the sources for debugging (i.e. with the option - -g of the Caml compiler) then add the -debug option at configuration - step : - - ./configure -debug <other options> - - and then compile the sources (step 5). Then you must make a Coq toplevel - including your own tactics, which must be compiled with -g, with coqmktop. - See the chapter 16 of the Coq Reference Manual for details about how - to use coqmktop and the Objective Caml debugger with Coq. + Unless you pass the -nodebug option to ./configure, the -g option of the + OCaml compiler will be used during compilation to allow debugging. + See the debugging file in dev/doc and the chapter 15 of the Coq Reference + Manual for details about how to use the OCaml debugger with Coq. THE AVAILABLE COMMANDS. |