This directory contains information and tools to help develop the Coq system

Debugging and profiling (dev/)

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 |

Miscellaneous information about the code (dev/doc)

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 |

Documentation of ML interfaces using ocamldoc ( dev/ocamldoc/html)

make mli-doc in coq root directory.

Other development tools (dev/tools)

| 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 |