More info on debugging: doc/debugging.md
| File | Description |
|---|---|
| dev/ocamldebug-coq | To launch ocaml debugger (generated by the configure script) |
| dev/db | To install pretty-printers from ocaml debugger |
| dev/base_db | To install raw pretty-printers from ocaml debugger |
| dev/include | To install pretty-printers from ocaml toplevel (use with the coq Drop command) |
| dev/base_include | To install raw pretty-printers from ocaml toplevel |
| dev/vm_printers.ml, top_printers.ml | ML pretty-printers for debugging |
Beginner's guide to hacking Coq: dev/doc/README.md
| File | Description |
|---|---|
dev/doc/changes.md |
(partial) Per-version summary of the evolution of Coq ML source |
dev/doc/style.txt |
A few style recommendations for writing Coq ML files |
dev/doc/debugging.md |
Help for debugging or profiling |
dev/doc/universes.txt |
Help for debugging universes |
dev/doc/extensions.txt |
Some help about TACTIC EXTEND |
dev/doc/perf-analysis |
Analysis of perfs measured on the compilation of user contribs |
dev/doc/cic.dtd |
Official dtd of the calc. of ind. constr. for im/ex-portation |
dev/doc/econstr.md |
Describes Econstr, implementation of treatment of evar in the engine |
dev/doc/primproj.md |
Describes primitive projections |
dev/doc/proof-engine.md |
Tutorial on new proof engine |
dev/doc/xml-protocol.md |
XML protocol that coqtop and IDEs use to communicate |
dev/doc/MERGING.md |
How pull requests should be merged into master |
dev/doc/release-process.md |
Process of creating a new Coq release |
make -f Makefile.dune apidoc in coq root directory.
| File | Description |
|---|---|
dev/tools/coqdev.el |
Helper customizations for everyday Coq development, eg making compile work in subdirectories |
dev/tools/objects.el |
Various development utilities at emacs level |