35 files changed, 39 insertions, 18 deletions
diff --git a/configure b/configure
index 5b031ccac..be6c2d0bc 100755
--- a/configure
+++ b/configure
@@ -575,11 +575,6 @@ if test "$coq_debug_flag" = "-g" ; then
   chmod a-w,a+x $OCAMLDEBUGCOQ
 fi
 
-# Compatibility with previous name
-if [ ! -f $COQTOP/dev/ocamldebug-v7 ] ; then
-  ln -s `basename $OCAMLDEBUGCOQ` $COQTOP/dev/ocamldebug-v7
-fi
-
 ##################################################
 # Fixing lablgtk types
 ####################################################
diff --git a/dev/README b/dev/README
index a8811beab..a4ca8f334 100644
--- a/dev/README
+++ b/dev/README
@@ -1,21 +1,47 @@
-This directory contains informations and tools to help developping the
-Coq system
+This directory contains informations and tools to help developing the
+                             Coq system
+                       ======================
 
 
-TODO
-changements.txt
-header
-lisezmoi.txt			   
-style.txt			   
+Debugging and profiling (in current directory - see doc/debugging.txt)
+-----------------------
 
-Debugging and profiling
-=======================
+ocamldebug-coq: to launch ocaml debugger
 
-debugging.txt: help for debugging or profiling
-db: to install pretty-printers from ocaml debugger
+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
+
+include:      to install pretty-printers from ocaml toplevel
 base_include: to install raw pretty-printers from ocaml toplevel
+
+vm_printers.ml, dev_printers.ml: ML pretty-printers for debugging
+
+
+Miscellaneous informations about the code (directory doc)
+-----------------------------------------
+
+changes.txt:   (partial) per-version summary of the evolutions of Coq ML source
+style.txt:     a few style recommendations for writing Coq ML files
+debugging.txt: help for debugging or profiling
 universes.txt: help to debug universes
+translate.txt: help to use coq translator
+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 tex (directory ocamlweb-doc)
+----------------------------------------
+
+go in directory and call "make"
+
+
+Other development tools (directory tools)
+-----------------------
+
 univdot: produces a graph of CIC universes
+Makefile.dir: makefile dedicated to intensive work in a given directory
+Makefile.subdir: makefile dedicated to intensive work in a given subdirectory
+Makefile.devel: utilities to automatically launch coq in various states
+Makefile.common: used by other Makefiles
+objects.el: various development utilities at emacs level
diff --git a/dev/changements.txt b/dev/doc/changes.txt
index d1df2a810..d1df2a810 100644
--- a/dev/changements.txt
+++ b/dev/doc/changes.txt
diff --git a/dev/cic.dtd b/dev/doc/cic.dtd
index f2314e224..f2314e224 100644
--- a/dev/cic.dtd
+++ b/dev/doc/cic.dtd
diff --git a/dev/debugging.txt b/dev/doc/debugging.txt
index e5c831396..e5c831396 100644
--- a/dev/debugging.txt
+++ b/dev/doc/debugging.txt
diff --git a/dev/header b/dev/doc/header
index 57945e47e..57945e47e 100644
--- a/dev/header
+++ b/dev/doc/header
diff --git a/dev/perf-analysis b/dev/doc/perf-analysis
index 232591569..232591569 100644
--- a/dev/perf-analysis
+++ b/dev/doc/perf-analysis
diff --git a/dev/style.txt b/dev/doc/style.txt
index 2e597dc45..2e597dc45 100644
--- a/dev/style.txt
+++ b/dev/doc/style.txt
diff --git a/dev/translate.txt b/dev/doc/translate.txt
index 5b372c96c..5b372c96c 100644
--- a/dev/translate.txt
+++ b/dev/doc/translate.txt
diff --git a/dev/universes.txt b/dev/doc/universes.txt
index 65c1e522a..65c1e522a 100644
--- a/dev/universes.txt
+++ b/dev/doc/universes.txt
diff --git a/dev/doc/Makefile b/dev/ocamlweb-doc/Makefile
index 964910173..964910173 100644
--- a/dev/doc/Makefile
+++ b/dev/ocamlweb-doc/Makefile
diff --git a/dev/doc/ast.ml b/dev/ocamlweb-doc/ast.ml
index 2153ef47c..2153ef47c 100644
--- a/dev/doc/ast.ml
+++ b/dev/ocamlweb-doc/ast.ml
diff --git a/dev/doc/interp.dep.ps b/dev/ocamlweb-doc/interp.dep.ps
index b05544812..b05544812 100644
--- a/dev/doc/interp.dep.ps
+++ b/dev/ocamlweb-doc/interp.dep.ps
diff --git a/dev/doc/intro.tex b/dev/ocamlweb-doc/intro.tex
index 4cec8673f..4cec8673f 100644
--- a/dev/doc/intro.tex
+++ b/dev/ocamlweb-doc/intro.tex
diff --git a/dev/doc/kernel.dep.ps b/dev/ocamlweb-doc/kernel.dep.ps
index 3c00121e8..3c00121e8 100644
--- a/dev/doc/kernel.dep.ps
+++ b/dev/ocamlweb-doc/kernel.dep.ps
diff --git a/dev/doc/lex.mll b/dev/ocamlweb-doc/lex.mll
index 617163e7e..617163e7e 100644
--- a/dev/doc/lex.mll
+++ b/dev/ocamlweb-doc/lex.mll
diff --git a/dev/doc/library.dep.ps b/dev/ocamlweb-doc/library.dep.ps
index 1c68240e7..1c68240e7 100644
--- a/dev/doc/library.dep.ps
+++ b/dev/ocamlweb-doc/library.dep.ps
diff --git a/dev/doc/macros.tex b/dev/ocamlweb-doc/macros.tex
index 6beacf7b0..6beacf7b0 100644
--- a/dev/doc/macros.tex
+++ b/dev/ocamlweb-doc/macros.tex
diff --git a/dev/doc/parse.ml b/dev/ocamlweb-doc/parse.ml
index e537b1f2f..e537b1f2f 100644
--- a/dev/doc/parse.ml
+++ b/dev/ocamlweb-doc/parse.ml
diff --git a/dev/doc/parsing.dep.ps b/dev/ocamlweb-doc/parsing.dep.ps
index 723d8c697..723d8c697 100644
--- a/dev/doc/parsing.dep.ps
+++ b/dev/ocamlweb-doc/parsing.dep.ps
diff --git a/dev/doc/preamble.tex b/dev/ocamlweb-doc/preamble.tex
index 2cd21f022..2cd21f022 100644
--- a/dev/doc/preamble.tex
+++ b/dev/ocamlweb-doc/preamble.tex
diff --git a/dev/doc/pretyping.dep.ps b/dev/ocamlweb-doc/pretyping.dep.ps
index 02d1b8b5a..02d1b8b5a 100644
--- a/dev/doc/pretyping.dep.ps
+++ b/dev/ocamlweb-doc/pretyping.dep.ps
diff --git a/dev/doc/proofs.dep.ps b/dev/ocamlweb-doc/proofs.dep.ps
index 0e78f4226..0e78f4226 100644
--- a/dev/doc/proofs.dep.ps
+++ b/dev/ocamlweb-doc/proofs.dep.ps
diff --git a/dev/doc/syntax.mly b/dev/ocamlweb-doc/syntax.mly
index bfc7d5ccf..bfc7d5ccf 100644
--- a/dev/doc/syntax.mly
+++ b/dev/ocamlweb-doc/syntax.mly
diff --git a/dev/doc/tactics.dep.ps b/dev/ocamlweb-doc/tactics.dep.ps
index f4de22b7e..f4de22b7e 100644
--- a/dev/doc/tactics.dep.ps
+++ b/dev/ocamlweb-doc/tactics.dep.ps
diff --git a/dev/doc/toplevel.dep.ps b/dev/ocamlweb-doc/toplevel.dep.ps
index e0355aac0..e0355aac0 100644
--- a/dev/doc/toplevel.dep.ps
+++ b/dev/ocamlweb-doc/toplevel.dep.ps
diff --git a/dev/Makefile.common b/dev/tools/Makefile.common
index 1ff5cf799..1ff5cf799 100644
--- a/dev/Makefile.common
+++ b/dev/tools/Makefile.common
diff --git a/dev/Makefile.devel b/dev/tools/Makefile.devel
index f3abb62dd..f3abb62dd 100644
--- a/dev/Makefile.devel
+++ b/dev/tools/Makefile.devel
diff --git a/dev/Makefile.dir b/dev/tools/Makefile.dir
index 54f7bfe9f..54f7bfe9f 100644
--- a/dev/Makefile.dir
+++ b/dev/tools/Makefile.dir
diff --git a/dev/Makefile.subdir b/dev/tools/Makefile.subdir
index 45358c426..45358c426 100644
--- a/dev/Makefile.subdir
+++ b/dev/tools/Makefile.subdir
diff --git a/dev/objects.el b/dev/tools/objects.el
index b3a2694d2..b3a2694d2 100644
--- a/dev/objects.el
+++ b/dev/tools/objects.el
diff --git a/dev/univdot b/dev/tools/univdot
index bb0dd2c89..bb0dd2c89 100755
--- a/dev/univdot
+++ b/dev/tools/univdot
diff --git a/dev/doc/check-grammar b/dev/v8-syntax/check-grammar
index 67da1bc51..67da1bc51 100755
--- a/dev/doc/check-grammar
+++ b/dev/v8-syntax/check-grammar
diff --git a/dev/doc/memo-v8.tex b/dev/v8-syntax/memo-v8.tex
index 8d116de26..8d116de26 100644
--- a/dev/doc/memo-v8.tex
+++ b/dev/v8-syntax/memo-v8.tex
diff --git a/dev/doc/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 97973df2b..97973df2b 100644
--- a/dev/doc/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex