diff options
| author |  Jim Fehrle <jfehrle@sbcglobal.net> | 2017-12-23 13:37:52 -0800 |
|---|---|---|
| committer |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-12-29 15:32:12 +0100 |
| commit | 2aeb740de93a0b32efe71bbd3a129e39bc6439e5 (patch) | |
| tree | 70160ddfb211aeed97d987a2bf1f451811300495 /dev/README | |
| parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) | |
Add instructions for debugging from the command line (and in Windows)
Avoid generating \r characters in generated dev/ocamldebug-coq (affects Windows)
Diffstat (limited to 'dev/README')
| -rw-r--r-- | dev/README | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/dev/README b/dev/README index b446c3e97..6b83579de 100644 --- a/dev/README +++ b/dev/README @@ -1,4 +1,4 @@ -This directory contains informations and tools to help developing the +This directory contains information and tools to help develop the Coq system ====================== @@ -6,30 +6,30 @@ This directory contains informations and tools to help developing the Debugging and profiling (in current directory - see doc/debugging.txt) ----------------------- -ocamldebug-coq: to launch ocaml debugger +ocamldebug-coq: to launch ocaml debugger (generated by the configure script) -db: to install pretty-printers from ocaml debugger -base_db: to install raw pretty-printers from ocaml debugger +db: to install pretty-printers from ocaml debugger +base_db: to install raw pretty-printers from ocaml debugger -include: to install pretty-printers from ocaml toplevel +include: to install pretty-printers from ocaml toplevel (use with the coq Drop command) base_include: to install raw pretty-printers from ocaml toplevel -vm_printers.ml, dev_printers.ml: ML pretty-printers for debugging +vm_printers.ml, top_printers.ml: ML pretty-printers for debugging -Miscellaneous informations about the code (directory doc) +Miscellaneous information about the code (directory doc) ----------------------------------------- -changes.txt: (partial) per-version summary of the evolutions of Coq ML source -style.txt: a few style recommendations for writing Coq ML files -debugging.txt: help for debugging or profiling -universes.txt: help to debug universes -translate.txt: help to use coq translator +changes.md: (partial) per-version summary of the evolution of Coq ML source +style.txt: a few style recommendations for writing Coq ML files +debugging.md: help for debugging or profiling +universes.txt: help for debugging universes +translate.txt: help for using coq translator extensions.txt: some help about TACTIC EXTEND -header: standard header for Coq ML files -perf-analysis: analysis of perfs measured on the compilation of user contribs -cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation +header: standard header for Coq ML files +perf-analysis: analysis of perfs measured on the compilation of user contribs +cic.dtd: official dtd of the calc. of ind. constr. for im/ex-portation Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) |