1 files changed, 46 insertions, 0 deletions
diff --git a/dev/README.md b/dev/README.md
new file mode 100644
index 00000000..4642aaf0
--- /dev/null
+++ b/dev/README.md
@@ -0,0 +1,46 @@
+# This directory contains information and tools to help develop the Coq system
+
+
+## Debugging and profiling (`dev/`)
+**More info on debugging: [`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.txt`](doc/universes.txt) |  Help for debugging universes |
+| [`dev/doc/extensions.txt`](doc/extensions.txt) | Some help about TACTIC EXTEND |
+| [`dev/doc/perf-analysis`](doc/perf-analysis)|  Analysis of perfs measured on the compilation of user contribs |
+| [`dev/doc/cic.dtd`](doc/cic.dtd) | Official dtd of the calc. of ind. constr. for im/ex-portation |
+| [`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/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine |
+| [`dev/doc/xml-protocol.md`](doc/proof-engine.md) | XML protocol that coqtop and IDEs use to communicate |
+| [`dev/doc/MERGING.md`](doc/MERGING.md) |  How pull requests should be merged into `master` |
+| [`dev/doc/release-process.md`](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`](tools/coqdev.el) | Helper customizations for everyday Coq development, eg making `compile` work in subdirectories
+| [`dev/tools/objects.el`](tools/objects.el) | Various development utilities at emacs level |