blob: 453f85f0d62a2e5d52e15eecef0b79453604d94f (
plain)
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
42
43
44
45
46
47
48
49
50
|
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.
|
