aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-12-19 12:19:42 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-12-19 12:19:42 +0000
commitc55728a42a8de6ce47bcb07d87050da5e5fc38f9 (patch)
tree4bd304755bfacaa701fe15a55da6d4172b65456d
parent5926ee209a0ad79ca14cf03bc6aadde86e9c35be (diff)
Pour les développeurs extérieurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2339 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--dev/README21
1 files changed, 21 insertions, 0 deletions
diff --git a/dev/README b/dev/README
new file mode 100644
index 000000000..a8811beab
--- /dev/null
+++ b/dev/README
@@ -0,0 +1,21 @@
+This directory contains informations and tools to help developping the
+Coq system
+
+
+TODO
+changements.txt
+header
+lisezmoi.txt
+style.txt
+
+Debugging and profiling
+=======================
+
+debugging.txt: help for debugging or profiling
+db: to install pretty-printers from ocaml debugger
+base_db: to install raw pretty-printers from ocaml debugger
+ocamldebug-v7: to launch ocaml debugger
+include: to install pretty-printers from ocaml toplevel
+base_include: to install raw pretty-printers from ocaml toplevel
+universes.txt: help to debug universes
+univdot: produces a graph of CIC universes