1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
# This directory contains information and tools to help develop the Coq system
## Debugging and profiling (`dev/`)
**More info on debugging: [`dev/doc/debugging.md`](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`](doc/README.md)**
| File | Description |
| ---- | ----------- |
| [`dev/doc/changes.md`](doc/changes.md) | (partial) Per-version summary of the evolution of Coq ML source |
| [`dev/doc/style.txt`](doc/style.txt) | A few style recommendations for writing Coq ML files |
| [`dev/doc/debugging.md`](doc/debugging.md) | Help for debugging or profiling |
| [`dev/doc/universes.md`](doc/universes.md) | Help for debugging universes |
| [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine |
| [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections |
| [`dev/doc/parsing.md`](doc/parsing.md) | Grammar and parsing overview |
| [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine |
| [`dev/doc/xml-protocol.md`](doc/xml-protocol.md) | XML protocol that coqtop and IDEs use to communicate |
| [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release |
## Documentation of ML interfaces using `odoc` ( `_build/default/_doc`)
`make apidoc` in coq root directory.
## Other development tools (`dev/tools`)
| File | Description |
| ---- | ----------- |
| [`dev/tools/coqdev.el`](tools/coqdev.el) | Helper customizations for everyday Coq development, eg making `compile` work in subdirectories
|
