diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-03 13:09:10 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-03 13:09:10 +0200 |
commit | 4deb788a24b50eec3da66ed32bb85c185123c007 (patch) | |
tree | 0996579af49d742b1723c2da12c962c93369bf97 /dev/README | |
parent | dbba44b5ea7608a66989b7fb065a0ef0b46ca7fe (diff) | |
parent | 5dfa8c9d9e3f1a5391825338498e0aaac28b4e28 (diff) |
Merge PR #7942: Extend readme with 'beginners guide'
Diffstat (limited to 'dev/README')
-rw-r--r-- | dev/README | 50 |
1 files changed, 0 insertions, 50 deletions
diff --git a/dev/README b/dev/README deleted file mode 100644 index 453f85f0d..000000000 --- a/dev/README +++ /dev/null @@ -1,50 +0,0 @@ -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. |