From 5dfa8c9d9e3f1a5391825338498e0aaac28b4e28 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 27 Jun 2018 23:29:00 +0200 Subject: Clean up documentation around beginner's guide. - move `README` to `README.md` to take advantage of markdown features - remove `setup.txt`, port the editor specific information to the wiki. Merge development information into `dev/doc/README.md`. Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup. - Add new links to files into `dev/README.md`. - Remove stale `translate.txt`. --- dev/README | 50 -------------------------------------------------- 1 file changed, 50 deletions(-) delete mode 100644 dev/README (limited to 'dev/README') 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. -- cgit v1.2.3