This directory contains information and tools to help develop the Rocq system #

Debugging and profiling (dev/) #

More info on debugging: dev/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 Rocq: dev/doc/README.md

File	Description
dev/doc/changes.md	(partial) Per-version summary of the evolution of Rocq ML source
dev/doc/style.txt	A few style recommendations for writing Rocq ML files
dev/doc/debugging.md	Help for debugging or profiling
dev/doc/universes.md	Help for debugging universes
dev/doc/econstr.md	Describes Econstr, implementation of treatment of evar in the engine
dev/doc/primproj.md	Describes primitive projections
dev/doc/parsing.md	Grammar and parsing overview
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/release-process.md	Process of creating a new Rocq 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	Helper customizations for everyday Rocq development, eg making compile work in subdirectories