Restructuration dossier dev et mise à jour de certaines documentations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7

35 files changed, 39 insertions, 18 deletions

diff --git a/configure b/configure
index 5b031ccac9..be6c2d0bca 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 a8811beab7..a4ca8f334a 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 d1df2a810b..d1df2a810b 100644
--- a/dev/changements.txt
+++ b/dev/doc/changes.txt
diff --git a/dev/cic.dtd b/dev/doc/cic.dtd
index f2314e224f..f2314e224f 100644
--- a/dev/cic.dtd
+++ b/dev/doc/cic.dtd
diff --git a/dev/debugging.txt b/dev/doc/debugging.txt
index e5c831396d..e5c831396d 100644
--- a/dev/debugging.txt
+++ b/dev/doc/debugging.txt
diff --git a/dev/header b/dev/doc/header
index 57945e47ea..57945e47ea 100644
--- a/dev/header
+++ b/dev/doc/header
diff --git a/dev/perf-analysis b/dev/doc/perf-analysis
index 232591569b..232591569b 100644
--- a/dev/perf-analysis
+++ b/dev/doc/perf-analysis
diff --git a/dev/style.txt b/dev/doc/style.txt
index 2e597dc45a..2e597dc45a 100644
--- a/dev/style.txt
+++ b/dev/doc/style.txt
diff --git a/dev/translate.txt b/dev/doc/translate.txt
index 5b372c96c3..5b372c96c3 100644
--- a/dev/translate.txt
+++ b/dev/doc/translate.txt
diff --git a/dev/universes.txt b/dev/doc/universes.txt
index 65c1e522af..65c1e522af 100644
--- a/dev/universes.txt
+++ b/dev/doc/universes.txt
diff --git a/dev/doc/Makefile b/dev/ocamlweb-doc/Makefile
index 9649101738..9649101738 100644
--- a/dev/doc/Makefile
+++ b/dev/ocamlweb-doc/Makefile
diff --git a/dev/doc/ast.ml b/dev/ocamlweb-doc/ast.ml
index 2153ef47c0..2153ef47c0 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 b055448121..b055448121 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 4cec8673f4..4cec8673f4 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 3c00121e81..3c00121e81 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 617163e7e7..617163e7e7 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 1c68240e74..1c68240e74 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 6beacf7b0b..6beacf7b0b 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 e537b1f2f4..e537b1f2f4 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 723d8c6976..723d8c6976 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 2cd21f0228..2cd21f0228 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 02d1b8b5a8..02d1b8b5a8 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 0e78f4226e..0e78f4226e 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 bfc7d5ccf0..bfc7d5ccf0 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 f4de22b7ef..f4de22b7ef 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 e0355aac04..e0355aac04 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 1ff5cf799e..1ff5cf799e 100644
--- a/dev/Makefile.common
+++ b/dev/tools/Makefile.common
diff --git a/dev/Makefile.devel b/dev/tools/Makefile.devel
index f3abb62dd8..f3abb62dd8 100644
--- a/dev/Makefile.devel
+++ b/dev/tools/Makefile.devel
diff --git a/dev/Makefile.dir b/dev/tools/Makefile.dir
index 54f7bfe9ff..54f7bfe9ff 100644
--- a/dev/Makefile.dir
+++ b/dev/tools/Makefile.dir
diff --git a/dev/Makefile.subdir b/dev/tools/Makefile.subdir
index 45358c426a..45358c426a 100644
--- a/dev/Makefile.subdir
+++ b/dev/tools/Makefile.subdir
diff --git a/dev/objects.el b/dev/tools/objects.el
index b3a2694d2c..b3a2694d2c 100644
--- a/dev/objects.el
+++ b/dev/tools/objects.el
diff --git a/dev/univdot b/dev/tools/univdot
index bb0dd2c89b..bb0dd2c89b 100755
--- a/dev/univdot
+++ b/dev/tools/univdot
diff --git a/dev/doc/check-grammar b/dev/v8-syntax/check-grammar
index 67da1bc513..67da1bc513 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 8d116de26f..8d116de26f 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 97973df2b6..97973df2b6 100644
--- a/dev/doc/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex