From c50f62734c6d180561c6a65679daef591d565944 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 11 Apr 2017 15:31:07 +0200 Subject: Update INSTALL now that -debug is the default. Also updates the references to debugging documentation. --- INSTALL | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 6b49738b8..eacbec299 100644 --- a/INSTALL +++ b/INSTALL @@ -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 - - 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. -- cgit v1.2.3