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


Debugging and profiling (in current directory - see doc/debugging.txt)
-----------------------

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

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, top_printers.ml: ML pretty-printers for debugging


Miscellaneous information about the code (directory doc)
-----------------------------------------

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


Documentation of ML interfaces using ocamldoc (directory ocamldoc/html)
----------------------------------------
"make mli-doc" in coq root directory.


Other development tools (directory tools)
-----------------------

coqdev.el: helper customizations for everyday Coq development, eg
  making `compile' work in subdirectories

objects.el: various development utilities at emacs level

anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse
  location of Anomaly backtraces and jump to them conveniently from
  the Emacs *compilation* output.