Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

38 files changed, 490 insertions, 37 deletions

diff --git a/dev/README b/dev/README
index a8811bea..0e40e820 100644
--- a/dev/README
+++ b/dev/README
@@ -1,21 +1,49 @@
-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
+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 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/base_include b/dev/base_include
index 30a6ed96..b7fa38ea 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -39,6 +39,108 @@
 #install_printer  (* bigint *) ppbigint;;
 #install_printer  (* loc *) pploc;;
 
+(* Open main files *)
+
+open Names
+open Term
+open Typeops
+open Univ
+open Inductive
+open Indtypes
+open Cooking
+open Closure
+open Reduction
+open Safe_typing
+open Declare
+open Declaremods
+open Impargs
+open Libnames
+open Nametab
+open Library
+
+open Cases
+open Pattern
+open Cbv
+open Classops
+open Pretyping
+open Cbv
+open Classops
+open Pretyping
+open Clenv
+open Rawterm
+open Coercion
+open Recordops
+open Detyping
+open Reductionops
+open Evarconv
+open Retyping
+open Evarutil
+open Tacred
+open Evd
+open Termops
+open Indrec
+open Typing
+open Inductiveops
+open Unification
+
+open Constrextern
+open Constrintern
+open Coqlib
+open Genarg
+open Modintern
+open Notation
+open Ppextend
+open Reserve
+open Syntax_def
+open Topconstr
+
+open Clenvtac
+open Evar_refiner
+open Logic
+open Pfedit
+open Proof_trees
+open Proof_type
+open Redexpr
+open Refiner
+open Tacmach
+
+open Auto
+open Autorewrite
+open Contradiction
+open Dhyp
+open Eauto
+open Elim
+open Equality
+open Evar_tactics
+open Extraargs
+open Extratactics
+open Hiddentac
+open Hipattern
+open Inv
+open Leminv
+open Refine
+open Setoid_replace
+open Tacinterp
+open Tacticals
+open Tactics
+
+open Cerrors
+open Class
+open Command
+open Coqinit
+open Coqtop
+open Discharge
+open Himsg
+open Metasyntax
+open Mltop
+open Record
+open Toplevel
+open Vernacentries
+open Vernacinterp
+open Vernac
+
+(* Various utilities *)
+
 let qid = Libnames.qualid_of_string;;
 
 (* parsing of terms *)
diff --git a/dev/db b/dev/db
index 6c657d4e..784e5bac 100644
--- a/dev/db
+++ b/dev/db
@@ -28,6 +28,7 @@ install_printer Top_printers.ppgoal
 install_printer Top_printers.ppsigmagoal
 install_printer Top_printers.pproof
 install_printer Top_printers.ppevd
+install_printer Top_printers.ppevm
 install_printer Top_printers.ppclenv
 
 install_printer Top_printers.pptac
diff --git a/dev/changements.txt b/dev/doc/changes.txt
index d1df2a81..f60e3203 100644
--- a/dev/changements.txt
+++ b/dev/doc/changes.txt
@@ -1,3 +1,49 @@
+=========================================
+= CHANGES BETWEEN COQ V8.0 AND COQ V8.1 =
+=========================================
+
+A few differences in Coq ML interfaces between Coq V8.0 and V8.1
+================================================================
+
+** Functions
+
+Util: option_app -> option_map
+Term: substl_decl -> subst_named_decl
+Lib: library_part -> remove_section_part
+Printer: prterm -> pr_lconstr
+Printer: prterm_env -> pr_lconstr_env
+Ppconstr: pr_sort -> pr_rawsort
+
+** Constructors
+
+Declarations: mind_consnrealargs -> mind_consnrealdecls
+NoRedun -> NoDup
+
+** Modules
+
+module Decl_kinds: new interface
+module Bigint: new interface
+module Tacred spawned module Redexpr
+module Symbols -> Notation
+module Coqast, Ast, Esyntax, Termast, and all other modules related to old
+  syntax are removed
+
+** Internal names
+
+OBJDEF and OBJDEF1 -> CANONICAL-STRUCTURE
+
+
+=========================================
+= CHANGES BETWEEN COQ V7.4 AND COQ V8.0 =
+=========================================
+
+See files in dev/syntax-v8
+
+
+==============================================
+= MAIN CHANGES BETWEEN COQ V7.3 AND COQ V7.4 =
+==============================================
+
 CHANGES DUE TO INTRODUCTION OF MODULES
 ======================================
 
@@ -183,8 +229,8 @@ Uses Declaremods to actually communicate with Global and to register
 objects.
 
 
-MAIN CHANGES FROM COQ V7.3
-==========================
+OTHER CHANGES
+=============
 
 Internal representation of tactics bindings has changed (see type
 Rawterm.substitution).
@@ -228,8 +274,10 @@ Tactics about False and not now in tactics/contradiction.ml
 Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v)
 File tacinterp.ml moved from proofs to directory tactics
 
-MAIN CHANGES FROM COQ V7.1 TO COQ V7.2
-======================================
+
+==========================================
+= MAIN CHANGES FROM COQ V7.1 TO COQ V7.2 =
+==========================================
 
 The core of Coq (kernel) has meen minimized with the following effects:
 
@@ -242,8 +290,9 @@ the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors,
 e.g. IsRel is now Rel, IsMutCase is now Case, etc.
 
 
-PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0
-===================================================
+=======================================================
+= PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0 =
+=======================================================
 
 Changements d'organisation / modules :
 --------------------------------------
diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd
new file mode 100644
index 00000000..f2314e22
--- /dev/null
+++ b/dev/doc/cic.dtd
@@ -0,0 +1,231 @@
+<?xml encoding="ISO-8859-1"?>
+
+<!-- DTD FOR CIC OBJECTS: -->
+
+<!-- CIC term declaration -->
+
+<!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST|
+                  LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'>
+
+<!-- CIC sorts -->
+
+<!ENTITY % sort '(Prop|Set|Type)'>
+
+<!-- CIC sequents -->
+
+<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'>
+
+<!-- CIC objects: -->
+
+<!ELEMENT ConstantType %term;>
+<!ATTLIST ConstantType
+          name       CDATA      #REQUIRED
+          id         ID         #REQUIRED>
+
+<!ELEMENT ConstantBody %term;>
+<!ATTLIST ConstantBody
+          for        CDATA      #REQUIRED
+          params     CDATA      #REQUIRED
+          id         ID         #REQUIRED>
+
+<!ELEMENT CurrentProof (Conjecture*,body)>
+<!ATTLIST CurrentProof
+          of         CDATA      #REQUIRED
+          id         ID         #REQUIRED>
+
+<!ELEMENT InductiveDefinition (InductiveType+)>
+<!ATTLIST InductiveDefinition
+          noParams NMTOKEN #REQUIRED
+          params   CDATA   #REQUIRED
+          id       ID      #REQUIRED>
+
+<!ELEMENT Variable (body?,type)>
+<!ATTLIST Variable
+          name CDATA #REQUIRED
+          id   ID    #REQUIRED>
+
+<!ELEMENT Sequent %sequent;>
+<!ATTLIST Sequent
+          no  NMTOKEN #REQUIRED
+          id  ID      #REQUIRED>
+
+<!-- Elements used in CIC objects, which are not terms: -->
+
+<!ELEMENT InductiveType (arity,Constructor*)>
+<!ATTLIST InductiveType
+          name      CDATA        #REQUIRED
+          inductive (true|false) #REQUIRED>
+
+<!ELEMENT Conjecture %sequent;>
+<!ATTLIST Conjecture
+          no NMTOKEN #REQUIRED
+          id ID      #REQUIRED>
+
+<!ELEMENT Constructor %term;>
+<!ATTLIST Constructor
+          name CDATA #REQUIRED>
+
+<!ELEMENT Decl %term;>
+<!ATTLIST Decl
+          name CDATA #IMPLIED
+          id   ID    #REQUIRED>
+
+<!ELEMENT Def %term;>
+<!ATTLIST Def
+          name CDATA #IMPLIED
+          id   ID    #REQUIRED>
+
+<!ELEMENT Hidden EMPTY>
+<!ATTLIST Hidden
+          id ID #REQUIRED>
+
+<!ELEMENT Goal %term;>
+
+<!-- CIC terms: -->
+
+<!ELEMENT LAMBDA (decl*,target)>
+<!ATTLIST LAMBDA
+          sort %sort; #REQUIRED>
+
+<!ELEMENT LETIN (def*,target)>
+<!ATTLIST LETIN
+          id   ID     #REQUIRED
+          sort %sort; #REQUIRED>
+
+<!ELEMENT PROD (decl*,target)>
+<!ATTLIST PROD
+          type %sort; #REQUIRED>
+
+<!ELEMENT CAST (term,type)>
+<!ATTLIST CAST
+          id   ID     #REQUIRED
+          sort %sort; #REQUIRED>
+
+<!ELEMENT REL EMPTY>
+<!ATTLIST REL
+          value  NMTOKEN #REQUIRED
+          binder CDATA   #REQUIRED
+          id     ID      #REQUIRED
+          idref  IDREF   #REQUIRED
+          sort   %sort;  #REQUIRED>
+
+<!ELEMENT SORT EMPTY>
+<!ATTLIST SORT
+          value CDATA #REQUIRED
+          id    ID    #REQUIRED>
+
+<!ELEMENT APPLY (%term;)+>
+<!ATTLIST APPLY
+          id   ID     #REQUIRED
+          sort %sort; #REQUIRED>
+
+<!ELEMENT VAR EMPTY>
+<!ATTLIST VAR
+          relUri CDATA  #REQUIRED
+          id     ID     #REQUIRED
+          sort   %sort; #REQUIRED>
+
+<!-- The substitutions are ordered by increasing DeBrujin  -->
+<!-- index. An empty substitution means that that index is -->
+<!-- not accessible.                                       -->
+<!ELEMENT META (substitution*)>
+<!ATTLIST META
+          no              NMTOKEN #REQUIRED
+          id              ID      #REQUIRED
+          sort            %sort;  #REQUIRED>
+
+<!ELEMENT IMPLICIT EMPTY>
+<!ATTLIST IMPLICIT
+          id ID #REQUIRED>
+
+<!ELEMENT CONST EMPTY>
+<!ATTLIST CONST
+          uri  CDATA  #REQUIRED
+          id   ID     #REQUIRED
+          sort %sort; #REQUIRED>
+
+<!ELEMENT MUTIND EMPTY>
+<!ATTLIST MUTIND
+          uri    CDATA   #REQUIRED
+          noType NMTOKEN #REQUIRED
+          id     ID      #REQUIRED>
+
+<!ELEMENT MUTCONSTRUCT EMPTY>
+<!ATTLIST MUTCONSTRUCT
+          uri      CDATA   #REQUIRED
+          noType   NMTOKEN #REQUIRED
+          noConstr NMTOKEN #REQUIRED
+          id       ID      #REQUIRED
+          sort     %sort;  #REQUIRED>
+
+<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)>
+<!ATTLIST MUTCASE
+          uriType CDATA   #REQUIRED
+          noType  NMTOKEN #REQUIRED
+          id      ID      #REQUIRED
+          sort    %sort;  #REQUIRED>
+
+<!ELEMENT FIX (FixFunction+)>
+<!ATTLIST FIX
+          noFun NMTOKEN #REQUIRED
+          id    ID      #REQUIRED
+          sort  %sort;  #REQUIRED>
+
+<!ELEMENT COFIX (CofixFunction+)>
+<!ATTLIST COFIX
+          noFun NMTOKEN #REQUIRED
+          id    ID      #REQUIRED
+          sort  %sort;  #REQUIRED>
+
+<!-- Elements used in CIC terms: -->
+
+<!ELEMENT FixFunction (type,body)>
+<!ATTLIST FixFunction
+          name     CDATA   #REQUIRED
+          recIndex NMTOKEN #REQUIRED>
+
+<!ELEMENT CofixFunction (type,body)>
+<!ATTLIST CofixFunction
+          name     CDATA   #REQUIRED>
+
+<!ELEMENT substitution ((%term;)?)>
+
+<!-- Explicit named substitutions: -->
+
+<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT),arg+)>
+<!ATTLIST instantiate
+          id ID #IMPLIED>
+
+<!-- Sintactic sugar for CIC terms and for CIC objects: -->
+
+<!ELEMENT arg %term;>
+<!ATTLIST arg
+          relUri CDATA #REQUIRED>
+
+<!ELEMENT decl %term;>
+<!ATTLIST decl
+          id     ID     #REQUIRED
+          type   %sort; #REQUIRED
+          binder CDATA  #IMPLIED>
+          
+<!ELEMENT def %term;>
+<!ATTLIST def
+          id     ID     #REQUIRED
+          sort   %sort; #REQUIRED
+          binder CDATA  #IMPLIED>
+
+<!ELEMENT target %term;>
+
+<!ELEMENT term %term;>
+
+<!ELEMENT type  %term;>
+
+<!ELEMENT arity %term;>
+
+<!ELEMENT patternsType  %term;>
+
+<!ELEMENT inductiveTerm  %term;>
+
+<!ELEMENT pattern  %term;>
+
+<!ELEMENT body  %term;>
diff --git a/dev/debugging.txt b/dev/doc/debugging.txt
index 4c04c42f..e5c83139 100644
--- a/dev/debugging.txt
+++ b/dev/doc/debugging.txt
@@ -1,4 +1,3 @@
-
 Debugging from Coq toplevel using Caml trace mechanism
 ======================================================
 
@@ -19,7 +18,6 @@ Debugging from Coq toplevel using Caml trace mechanism
 Debugging from Caml debugger
 ============================
 
-   Preferably use ocaml 3.06 (pretty-printing is broken with ocaml 3.07/3.08)
    Needs tuareg mode in Emacs
    Coq must be configured with -debug and -local (./configure -debug -local)
 
@@ -44,13 +42,30 @@ Debugging from Caml debugger
      Vernac.vernac_com at the with clause of the "try ... interp com
      with ..." block, then go "back" a few steps to find where the
      failure/error/anomaly has been raised
-   - If "source db" fails, first recompile top_printers.ml with
-     "make dev/top_printers.cmo"
+   - Alternatively, for an error or an anomaly, add breakpoints in the middle  
+     of each of error* functions or anomaly* functions in lib/util.ml
+   - If "source db" fails, recompile printers.cma with
+     "make dev/printers.cma" and try again
 
-Profiling
-=========
+Global gprof-based profiling
+============================
 
    Coq must be configured with option -profile
 
    1. Run native Coq which must end normally (use Quit or option -batch)
    2. gprof ./coqtop gmon.out
+
+Per function profiling
+======================
+
+   1. To profile function foo in file bar.ml, add the following lines, just
+      after the definition of the function:
+
+     let fookey = Profile.declare_profile "foo";;
+     let foo a b c = Profile.profile3 fookey foo a b c;;
+
+     where foo is assumed to have three arguments (adapt using
+     Profile.profile1, Profile. profile2, etc).
+
+     This has the effect to cumulate the time passed in foo under a
+     line of name "foo" which is displayed at the time coqtop exits.
diff --git a/dev/doc/extensions.txt b/dev/doc/extensions.txt
new file mode 100644
index 00000000..eb4d2659
--- /dev/null
+++ b/dev/doc/extensions.txt
@@ -0,0 +1,19 @@
+Comment ajouter une nouvelle entrée primitive pour les TACTIC EXTEND ?
+======================================================================
+
+Exemple de l'ajout de l'entrée "clause":
+
+- ajouter un type ClauseArgType dans interp/genarg.ml{,i}, avec les
+  wit_, rawwit_, et globwit_ correspondants
+
+- ajouter partout où Genarg.argument_type est filtré le cas traitant de
+  ce nouveau ClauseArgType
+
+- utiliser le rawwit_clause pour définir une entrée clause du bon
+  type et du bon nom dans le module Tactic de pcoq.ml4
+
+- il faut aussi exporter la règle hors de g_tactic.ml4. Pour cela, il
+  faut rejouter clause dans le GLOBAL du GEXTEND
+
+- seulement après, le nom clause sera accessible dans les TACTIC EXTEND !
+
diff --git a/dev/header b/dev/doc/header
index 57945e47..57945e47 100644
--- a/dev/header
+++ b/dev/doc/header
diff --git a/dev/perf-analysis b/dev/doc/perf-analysis
index 23259156..23259156 100644
--- a/dev/perf-analysis
+++ b/dev/doc/perf-analysis
diff --git a/dev/style.txt b/dev/doc/style.txt
index 2e597dc4..2e597dc4 100644
--- a/dev/style.txt
+++ b/dev/doc/style.txt
diff --git a/dev/translate.txt b/dev/doc/translate.txt
index 5b372c96..5b372c96 100644
--- a/dev/translate.txt
+++ b/dev/doc/translate.txt
diff --git a/dev/universes.txt b/dev/doc/universes.txt
index 65c1e522..65c1e522 100644
--- a/dev/universes.txt
+++ b/dev/doc/universes.txt
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
index 30224216..5c4c4475 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.template
@@ -36,7 +36,7 @@ case $coqdebug in
         -I $COQTOP/contrib/interface  -I $COQTOP/contrib/jprover \
         -I $COQTOP/contrib/omega      -I $COQTOP/contrib/romega \
         -I $COQTOP/contrib/ring       -I $COQTOP/contrib/xml \
-	-I $COQTOP/contrib/subtac \
+	-I $COQTOP/contrib/subtac     -I $COQTOP/contrib/funind \
 	$* $args;;
     *) exec $OCAMLDEBUG $*;;
 esac
diff --git a/dev/doc/Makefile b/dev/ocamlweb-doc/Makefile
index a0bef897..96491017 100644
--- a/dev/doc/Makefile
+++ b/dev/ocamlweb-doc/Makefile
@@ -1,7 +1,7 @@
 
 # Makefile for doc/
 
-all:: newparse 
+all:: newparse coq.ps minicop.ps
 #newsyntax.dvi minicoq.dvi
 
 
@@ -10,19 +10,19 @@ OBJS=lex.cmo ast.cmo parse.cmo syntax.cmo
 newparse: $(OBJS) syntax.mli lex.ml syntax.ml
 	ocamlc -o newparse $(OBJS)
 
-.ml.cmo:
+%.cmo: %.ml
 	ocamlc -c $<
 
-.mli.cmi:
+%.cmi: %.mli
 	ocamlc -c $<
 
-.mll.ml:
+%.ml: %.mll
 	ocamllex $<
 
-.mly.ml:
+%.ml: %.mly
 	ocamlyacc -v $<
 
-.mly.mli:
+%.mli: %.mly
 	ocamlyacc -v $<
 
 clean::
@@ -43,7 +43,14 @@ coq.dvi: coq.tex
 	latex coq
 
 coq.tex::
-	make -C .. doc/coq.tex
+	ocamlweb -p "\usepackage{epsfig}" \
+	macros.tex intro.tex \
+	../../lib/{doc.tex,*.mli} ../../kernel/{doc.tex,*.mli} ../../library/{doc.tex,*.mli} \
+	../../pretyping/{doc.tex,*.mli} ../../interp/{doc.tex,*.mli} \
+	../../parsing/{doc.tex,*.mli} ../../proofs/{doc.tex,*.mli} \
+	../../tactics/{doc.tex,*.mli} ../../toplevel/{doc.tex,*.mli} \
+	-o coq.tex
+
 
 depend:: kernel.dep.ps library.dep.ps pretyping.dep.ps parsing.dep.ps \
          proofs.dep.ps tactics.dep.ps toplevel.dep.ps interp.dep.ps
@@ -59,9 +66,10 @@ clean::
 
 .SUFFIXES: .tex .dvi .ps .cmo .cmi .mli .ml .mll .mly
 
-.tex.dvi:
+%.dvi: %.tex
 	latex $< && latex $<
 
-.dvi.ps:
+%.ps: %.dvi
 	dvips $< -o $@
 
+
diff --git a/dev/doc/ast.ml b/dev/ocamlweb-doc/ast.ml
index 2153ef47..2153ef47 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 b0554481..b0554481 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 4cec8673..4cec8673 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 3c00121e..3c00121e 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 617163e7..617163e7 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 1c68240e..1c68240e 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 6beacf7b..6beacf7b 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 e537b1f2..e537b1f2 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 723d8c69..723d8c69 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 2cd21f02..2cd21f02 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 02d1b8b5..02d1b8b5 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 0e78f422..0e78f422 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 bfc7d5cc..bfc7d5cc 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 f4de22b7..f4de22b7 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 e0355aac..e0355aac 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 1ff5cf79..1ff5cf79 100644
--- a/dev/Makefile.common
+++ b/dev/tools/Makefile.common
diff --git a/dev/Makefile.devel b/dev/tools/Makefile.devel
index f3abb62d..f3abb62d 100644
--- a/dev/Makefile.devel
+++ b/dev/tools/Makefile.devel
diff --git a/dev/Makefile.dir b/dev/tools/Makefile.dir
index 54f7bfe9..68c917ac 100644
--- a/dev/Makefile.dir
+++ b/dev/tools/Makefile.dir
@@ -17,7 +17,7 @@ test-dir:
 	@echo TOPDIR=$(TOPDIR)
 	@echo BASEDIR=$(BASEDIR)
 
-include $(TOPDIR)/dev/Makefile.common
+include $(TOPDIR)/dev/tools/Makefile.common
 
 # make this directory
 dir:
diff --git a/dev/Makefile.subdir b/dev/tools/Makefile.subdir
index 45358c42..ff1f3077 100644
--- a/dev/Makefile.subdir
+++ b/dev/tools/Makefile.subdir
@@ -4,4 +4,4 @@
 # in order to have all the facilities of dev/Makefile.dir
 
 TOPDIR=../..
-include $(TOPDIR)/dev/Makefile.dir
+include $(TOPDIR)/dev/tools/Makefile.dir
diff --git a/dev/objects.el b/dev/tools/objects.el
index b3a2694d..b3a2694d 100644
--- a/dev/objects.el
+++ b/dev/tools/objects.el
diff --git a/dev/univdot b/dev/tools/univdot
index bb0dd2c8..bb0dd2c8 100755
--- a/dev/univdot
+++ b/dev/tools/univdot
diff --git a/dev/doc/check-grammar b/dev/v8-syntax/check-grammar
index 67da1bc5..67da1bc5 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 8d116de2..8d116de2 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 97973df2..97973df2 100644
--- a/dev/doc/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex