Remove obsolete files from dev/doc

- cic.dtd is related to the XML plugin
- about-hints uses v7 syntax
- minicoq.tex talks about a tool that is not there
- translate.txt talks about the v7->v8 translation machinery
- transition-* talk about v5->v7 changes to the sources layout

6 files changed, 0 insertions, 1291 deletions

diff --git a/dev/doc/about-hints b/dev/doc/about-hints
deleted file mode 100644
index 95712c3cf9..0000000000
--- a/dev/doc/about-hints
+++ /dev/null
@@ -1,454 +0,0 @@
-An investigation of how ZArith lemmas could be classified in different
-automation classes
-
-- Reversible lemmas relating operators (to be declared as hints but
-  needing precedences)
-- Equivalent notions (one has to be considered as primitive and the
-  other rewritten into the canonical one)
-- Isomorphisms between structure (one structure has to be considered
-  as more primitive than the other for a give operator)
-- Irreversible simplifications (to be declared with precedences)
-- Reversible bottom-up simplifications (to be used in hypotheses)
-- Irreversible bottom-up simplifications (to be used in hypotheses
-  with precedences)
-- Rewriting rules (relevant for autorewrite, or for an improved auto)
-
-Note: this analysis, made in 2001, was previously stored in
-theories/ZArith/Zhints.v. It has been moved here to avoid obfuscating
-the standard library.
-
-(**********************************************************************)
-(** *        Reversible lemmas relating operators                     *)
-(** Probably to be declared as hints but need to define precedences   *)
-
-(** ** Conversion between comparisons/predicates and arithmetic operators *)
-
-(** Lemmas ending by eq *)
-(**
-<<
-Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0`
-Zabs_eq: (x:Z)`0 <= x`->`|x| = x`
-Zeven_div2: (x:Z)(Zeven x)->`x = 2*(Zdiv2 x)`
-Zodd_div2: (x:Z)`x >= 0`->(Zodd x)->`x = 2*(Zdiv2 x)+1`
->>
-*)
-
-(** Lemmas ending by Zgt *)
-(**
-<<
-Zgt_left_rev: (x,y:Z)`x+(-y) > 0`->`x > y`
-Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0`
->>
-*)
-
-(** Lemmas ending by Zlt *)
-(**
-<<
-Zlt_left_rev: (x,y:Z)`0 < y+(-x)`->`x < y`
-Zlt_left_lt: (x,y:Z)`x < y`->`0 < y+(-x)`
-Zlt_O_minus_lt: (n,m:Z)`0 < n-m`->`m < n`
->>
-*)
-
-(** Lemmas ending by Zle *)
-(**
-<<
-Zle_left: (x,y:Z)`x <= y`->`0 <= y+(-x)`
-Zle_left_rev: (x,y:Z)`0 <= y+(-x)`->`x <= y`
-Zlt_left: (x,y:Z)`x < y`->`0 <= y+(-1)+(-x)`
-Zge_left: (x,y:Z)`x >= y`->`0 <= x+(-y)`
-Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)`
->>
-*)
-
-(** ** Conversion between nat comparisons and Z comparisons *)
-
-(** Lemmas ending by eq *)
-(**
-<<
-inj_eq: (x,y:nat)x=y->`(inject_nat x) = (inject_nat y)`
->>
-*)
-
-(** Lemmas ending by Zge *)
-(**
-<<
-inj_ge: (x,y:nat)(ge x y)->`(inject_nat x) >= (inject_nat y)`
->>
-*)
-
-(** Lemmas ending by Zgt *)
-(**
-<<
-inj_gt: (x,y:nat)(gt x y)->`(inject_nat x) > (inject_nat y)`
->>
-*)
-
-(** Lemmas ending by Zlt *)
-(**
-<<
-inj_lt: (x,y:nat)(lt x y)->`(inject_nat x) < (inject_nat y)`
->>
-*)
-
-(** Lemmas ending by Zle *)
-(**
-<<
-inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)`
->>
-*)
-
-(** ** Conversion between comparisons *)
-
-(** Lemmas ending by Zge *)
-(**
-<<
-not_Zlt: (x,y:Z)~`x < y`->`x >= y`
-Zle_ge: (m,n:Z)`m <= n`->`n >= m`
->>
-*)
-
-(** Lemmas ending by Zgt *)
-(**
-<<
-Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n`
-not_Zle: (x,y:Z)~`x <= y`->`x > y`
-Zlt_gt: (m,n:Z)`m < n`->`n > m`
-Zle_S_gt: (n,m:Z)`(Zs n) <= m`->`m > n`
->>
-*)
-
-(** Lemmas ending by Zlt *)
-(**
-<<
-not_Zge: (x,y:Z)~`x >= y`->`x < y`
-Zgt_lt: (m,n:Z)`m > n`->`n < m`
-Zle_lt_n_Sm: (n,m:Z)`n <= m`->`n < (Zs m)`
->>
-*)
-
-(** Lemmas ending by Zle *)
-(**
-<<
-Zlt_ZERO_pred_le_ZERO: (x:Z)`0 < x`->`0 <= (Zpred x)`
-not_Zgt: (x,y:Z)~`x > y`->`x <= y`
-Zgt_le_S: (n,p:Z)`p > n`->`(Zs n) <= p`
-Zgt_S_le: (n,p:Z)`(Zs p) > n`->`n <= p`
-Zge_le: (m,n:Z)`m >= n`->`n <= m`
-Zlt_le_S: (n,p:Z)`n < p`->`(Zs n) <= p`
-Zlt_n_Sm_le: (n,m:Z)`n < (Zs m)`->`n <= m`
-Zlt_le_weak: (n,m:Z)`n < m`->`n <= m`
-Zle_refl: (n,m:Z)`n = m`->`n <= m`
->>
-*)
-
-(** ** Irreversible simplification involving several comparaisons *)
-(**    useful with clear precedences *)
-
-(** Lemmas ending by Zlt *)
-(**
-<<
-Zlt_le_reg :(a,b,c,d:Z)`a < b`->`c <= d`->`a+c < b+d`
-Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d`
->>
-*)
-
-(** ** What is decreasing here ? *)
-
-(** Lemmas ending by eq *)
-(**
-<<
-Zplus_minus: (n,m,p:Z)`n = m+p`->`p = n-m`
->>
-*)
-
-(** Lemmas ending by Zgt *)
-(**
-<<
-Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n`
->>
-*)
-
-(** Lemmas ending by Zlt *)
-(**
-<<
-Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)`
->>
-*)
-
-(**********************************************************************)
-(** *                Useful Bottom-up lemmas                          *)
-
-(** ** Bottom-up simplification: should be used *)
-
-(** Lemmas ending by eq *)
-(**
-<<
-Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m`
-Zsimpl_plus_l: (n,m,p:Z)`n+m = n+p`->`m = p`
-Zplus_unit_left: (n,m:Z)`n+0 = m`->`n = m`
-Zplus_unit_right: (n,m:Z)`n = m+0`->`n = m`
->>
-*)
-
-(** Lemmas ending by Zgt *)
-(**
-<<
-Zsimpl_gt_plus_l: (n,m,p:Z)`p+n > p+m`->`n > m`
-Zsimpl_gt_plus_r: (n,m,p:Z)`n+p > m+p`->`n > m`
-Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n`
->>
-*)
-
-(** Lemmas ending by Zlt *)
-(**
-<<
-Zsimpl_lt_plus_l: (n,m,p:Z)`p+n < p+m`->`n < m`
-Zsimpl_lt_plus_r: (n,m,p:Z)`n+p < m+p`->`n < m`
-Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m`
->>
-*)
-
-(** Lemmas ending by Zle *)
-(** << Zsimpl_le_plus_l: (p,n,m:Z)`p+n <= p+m`->`n <= m`
-Zsimpl_le_plus_r: (p,n,m:Z)`n+p <= m+p`->`n <= m`
-Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n` >> *)
-
-(** ** Bottom-up irreversible (syntactic) simplification *)
-
-(** Lemmas ending by Zle *)
-(**
-<<
-Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m`
->>
-*)
-
-(** ** Other unclearly simplifying lemmas *)
-
-(** Lemmas ending by Zeq *)
-(**
-<<
-Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0`
->>
-*)
-
-(* Lemmas ending by Zgt *)
-(**
-<<
-Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0`
->>
-*)
-
-(* Lemmas ending by Zlt *)
-(**
-<<
-pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y`
->>
-*)
-
-(* Lemmas ending by Zle *)
-(**
-<<
-Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y`
-OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y`
->>
-*)
-
-
-(**********************************************************************)
-(** *        Irreversible lemmas with meta-variables                  *)
-(** To be used by EAuto                                               *)
-
-(* Hints Immediate *)
-(** Lemmas ending by eq *)
-(**
-<<
-Zle_antisym: (n,m:Z)`n <= m`->`m <= n`->`n = m`
->>
-*)
-
-(** Lemmas ending by Zge *)
-(**
-<<
-Zge_trans: (n,m,p:Z)`n >= m`->`m >= p`->`n >= p`
->>
-*)
-
-(** Lemmas ending by Zgt *)
-(**
-<<
-Zgt_trans: (n,m,p:Z)`n > m`->`m > p`->`n > p`
-Zgt_trans_S: (n,m,p:Z)`(Zs n) > m`->`m > p`->`n > p`
-Zle_gt_trans: (n,m,p:Z)`m <= n`->`m > p`->`n > p`
-Zgt_le_trans: (n,m,p:Z)`n > m`->`p <= m`->`n > p`
->>
-*)
-
-(** Lemmas ending by Zlt *)
-(**
-<<
-Zlt_trans: (n,m,p:Z)`n < m`->`m < p`->`n < p`
-Zlt_le_trans: (n,m,p:Z)`n < m`->`m <= p`->`n < p`
-Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p`
->>
-*)
-
-(** Lemmas ending by Zle *)
-(**
-<<
-Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p`
->>
-*)
-
-
-(**********************************************************************)
-(** *               Unclear or too specific lemmas                    *)
-(** Not to be used ?                                                  *)
-
-(** ** Irreversible and too specific (not enough regular) *)
-
-(** Lemmas ending by Zle *)
-(**
-<<
-Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x`
-Zle_mult_approx: (x,y,z:Z)`x > 0`->`z > 0`->`0 <= y`->`0 <= y*x+z`
-OMEGA6: (x,y,z:Z)`0 <= x`->`y = 0`->`0 <= x+y*z`
-OMEGA7: (x,y,z,t:Z)`z > 0`->`t > 0`->`0 <= x`->`0 <= y`->`0 <= x*z+y*t`
->>
-*)
-
-(** ** Expansion and too specific ? *)
-
-(** Lemmas ending by Zge *)
-(**
-<<
-Zge_mult_simpl: (a,b,c:Z)`c > 0`->`a*c >= b*c`->`a >= b`
->>
-*)
-
-(** Lemmas ending by Zgt *)
-(**
-<<
-Zgt_mult_simpl: (a,b,c:Z)`c > 0`->`a*c > b*c`->`a > b`
-Zgt_square_simpl: (x,y:Z)`x >= 0`->`y >= 0`->`x*x > y*y`->`x > y`
->>
-*)
-
-(** Lemmas ending by Zle *)
-(**
-<<
-Zle_mult_simpl: (a,b,c:Z)`c > 0`->`a*c <= b*c`->`a <= b`
-Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y`
->>
-*)
-
-(** ** Reversible but too specific ? *)
-
-(** Lemmas ending by Zlt *)
-(**
-<<
-Zlt_minus: (n,m:Z)`0 < m`->`n-m < n`
->>
-*)
-
-(**********************************************************************)
-(** *               Lemmas to be used as rewrite rules                *)
-(** but can also be used as hints                                     *)
-
-(** Left-to-right simplification lemmas (a symbol disappears) *)
-
-(**
-<<
-Zcompare_n_S: (n,m:Z)(Zcompare (Zs n) (Zs m))=(Zcompare n m)
-Zmin_n_n: (n:Z)`(Zmin n n) = n`
-Zmult_1_n: (n:Z)`1*n = n`
-Zmult_n_1: (n:Z)`n*1 = n`
-Zminus_plus: (n,m:Z)`n+m-n = m`
-Zle_plus_minus: (n,m:Z)`n+(m-n) = m`
-Zopp_Zopp: (x:Z)`(-(-x)) = x`
-Zero_left: (x:Z)`0+x = x`
-Zero_right: (x:Z)`x+0 = x`
-Zplus_inverse_r: (x:Z)`x+(-x) = 0`
-Zplus_inverse_l: (x:Z)`(-x)+x = 0`
-Zopp_intro: (x,y:Z)`(-x) = (-y)`->`x = y`
-Zmult_one: (x:Z)`1*x = x`
-Zero_mult_left: (x:Z)`0*x = 0`
-Zero_mult_right: (x:Z)`x*0 = 0`
-Zmult_Zopp_Zopp: (x,y:Z)`(-x)*(-y) = x*y`
->>
-*)
-
-(** Right-to-left simplification lemmas (a symbol disappears) *)
-
-(**
-<<
-Zpred_Sn: (m:Z)`m = (Zpred (Zs m))`
-Zs_pred: (n:Z)`n = (Zs (Zpred n))`
-Zplus_n_O: (n:Z)`n = n+0`
-Zmult_n_O: (n:Z)`0 = n*0`
-Zminus_n_O: (n:Z)`n = n-0`
-Zminus_n_n: (n:Z)`0 = n-n`
-Zred_factor6: (x:Z)`x = x+0`
-Zred_factor0: (x:Z)`x = x*1`
->>
-*)
-
-(** Unclear orientation (no symbol disappears) *)
-
-(**
-<<
-Zplus_n_Sm: (n,m:Z)`(Zs (n+m)) = n+(Zs m)`
-Zmult_n_Sm: (n,m:Z)`n*m+n = n*(Zs m)`
-Zmin_SS: (n,m:Z)`(Zs (Zmin n m)) = (Zmin (Zs n) (Zs m))`
-Zplus_assoc_l: (n,m,p:Z)`n+(m+p) = n+m+p`
-Zplus_assoc_r: (n,m,p:Z)`n+m+p = n+(m+p)`
-Zplus_permute: (n,m,p:Z)`n+(m+p) = m+(n+p)`
-Zplus_Snm_nSm: (n,m:Z)`(Zs n)+m = n+(Zs m)`
-Zminus_plus_simpl: (n,m,p:Z)`n-m = p+n-(p+m)`
-Zminus_Sn_m: (n,m:Z)`(Zs (n-m)) = (Zs n)-m`
-Zmult_plus_distr_l: (n,m,p:Z)`(n+m)*p = n*p+m*p`
-Zmult_minus_distr: (n,m,p:Z)`(n-m)*p = n*p-m*p`
-Zmult_assoc_r: (n,m,p:Z)`n*m*p = n*(m*p)`
-Zmult_assoc_l: (n,m,p:Z)`n*(m*p) = n*m*p`
-Zmult_permute: (n,m,p:Z)`n*(m*p) = m*(n*p)`
-Zmult_Sm_n: (n,m:Z)`n*m+m = (Zs n)*m`
-Zmult_Zplus_distr: (x,y,z:Z)`x*(y+z) = x*y+x*z`
-Zmult_plus_distr: (n,m,p:Z)`(n+m)*p = n*p+m*p`
-Zopp_Zplus: (x,y:Z)`(-(x+y)) = (-x)+(-y)`
-Zplus_sym: (x,y:Z)`x+y = y+x`
-Zplus_assoc: (x,y,z:Z)`x+(y+z) = x+y+z`
-Zmult_sym: (x,y:Z)`x*y = y*x`
-Zmult_assoc: (x,y,z:Z)`x*(y*z) = x*y*z`
-Zopp_Zmult: (x,y:Z)`(-x)*y = (-(x*y))`
-Zplus_S_n: (x,y:Z)`(Zs x)+y = (Zs (x+y))`
-Zopp_one: (x:Z)`(-x) = x*(-1)`
-Zopp_Zmult_r: (x,y:Z)`(-(x*y)) = x*(-y)`
-Zmult_Zopp_left: (x,y:Z)`(-x)*y = x*(-y)`
-Zopp_Zmult_l: (x,y:Z)`(-(x*y)) = (-x)*y`
-Zred_factor1: (x:Z)`x+x = x*2`
-Zred_factor2: (x,y:Z)`x+x*y = x*(1+y)`
-Zred_factor3: (x,y:Z)`x*y+x = x*(1+y)`
-Zred_factor4: (x,y,z:Z)`x*y+x*z = x*(y+z)`
-Zminus_Zplus_compatible: (x,y,n:Z)`x+n-(y+n) = x-y`
-Zmin_plus: (x,y,n:Z)`(Zmin (x+n) (y+n)) = (Zmin x y)+n`
->>
-*)
-
-(** nat <-> Z *)
-(**
-<<
-inj_S: (y:nat)`(inject_nat (S y)) = (Zs (inject_nat y))`
-inj_plus: (x,y:nat)`(inject_nat (plus x y)) = (inject_nat x)+(inject_nat y)`
-inj_mult: (x,y:nat)`(inject_nat (mult x y)) = (inject_nat x)*(inject_nat y)`
-inj_minus1:
- (x,y:nat)(le y x)->`(inject_nat (minus x y)) = (inject_nat x)-(inject_nat y)`
-inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0`
->>
-*)
-
-(** Too specific ? *)
-(**
-<<
-Zred_factor5: (x,y:Z)`x*0+y = y`
->>
-*)
diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd
deleted file mode 100644
index cc33efd483..0000000000
--- a/dev/doc/cic.dtd
+++ /dev/null
@@ -1,231 +0,0 @@
-<?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 de Bruijn  -->
-<!-- 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/doc/minicoq.tex b/dev/doc/minicoq.tex
deleted file mode 100644
index a34b03a491..0000000000
--- a/dev/doc/minicoq.tex
+++ /dev/null
@@ -1,98 +0,0 @@
-\documentclass{article}
-
-\usepackage{fullpage}
-\input{./macros.tex}
-\newcommand{\minicoq}{\textsf{minicoq}}
-\newcommand{\nonterm}[1]{\textit{#1}}
-\newcommand{\terminal}[1]{\textsf{#1}}
-\newcommand{\listzero}{\textit{LIST$_0$}}
-\newcommand{\listun}{\textit{LIST$_1$}}
-\newcommand{\sep}{\textit{SEP}}
-
-\title{Minicoq: a type-checker for the pure \\ 
-       Calculus of Inductive Constructions}
-
-
-\begin{document}
-
-\maketitle
-
-\section{Introduction}
-
-\minicoq\ is a minimal toplevel for the \Coq\ kernel.
-
-
-\section{Grammar of terms}
-
-The grammar of \minicoq's terms is given in Figure~\ref{fig:terms}. 
-
-\begin{figure}[htbp]
-  \hrulefill
-  \begin{center}
-    \begin{tabular}{lrl}
-      term & ::= & identifier \\
-           & $|$ & \terminal{Rel} integer \\
-           & $|$ & \terminal{Set} \\
-           & $|$ & \terminal{Prop} \\
-           & $|$ & \terminal{Type} \\
-           & $|$ & \terminal{Const} identifier \\
-           & $|$ & \terminal{Ind} identifier integer \\
-           & $|$ & \terminal{Construct} identifier integer integer \\
-           & $|$ & \terminal{[} name \terminal{:} term
-                   \terminal{]} term \\
-           & $|$ & \terminal{(} name \terminal{:} term
-                   \terminal{)} term \\
-           & $|$ & term \verb!->! term \\
-           & $|$ & \terminal{(} \listun\ term \terminal{)} \\
-           & $|$ & \terminal{(} term \terminal{::} term \terminal{)} \\
-           & $|$ & \verb!<! term \verb!>! \terminal{Case}
-                   term \terminal{of} \listzero\ term \terminal{end} 
-      \\[1em]
-      name & ::= & \verb!_! \\
-           & $|$ & identifier 
-   \end{tabular}
-  \end{center}
-  \hrulefill
-  \caption{Grammar of terms}
-  \label{fig:terms}
-\end{figure}
-
-\section{Commands}
-The grammar of \minicoq's commands are given in
-Figure~\ref{fig:commands}. All commands end with a dot.
-
-\begin{figure}[htbp]
-  \hrulefill
-  \begin{center}
-    \begin{tabular}{lrl}
-      command & ::= & \terminal{Definition} identifier \terminal{:=} term. \\
-              & $|$ & \terminal{Definition} identifier \terminal{:} term
-                      \terminal{:=} term. \\
-              & $|$ & \terminal{Parameter} identifier \terminal{:} term. \\
-              & $|$ & \terminal{Variable} identifier \terminal{:} term. \\
-              & $|$ & \terminal{Inductive} \terminal{[} \listzero\ param 
-                      \terminal{]} \listun\ inductive \sep\ 
-                      \terminal{with}. \\
-              & $|$ & \terminal{Check} term. 
-      \\[1em]
-      param   & ::= & identifier 
-      \\[1em]
-      inductive & ::= & identifier \terminal{:} term \terminal{:=}
-                        \listzero\ constructor \sep\ \terminal{$|$}
-      \\[1em]
-      constructor & ::= & identifier \terminal{:} term
-    \end{tabular}
-  \end{center}
-  \hrulefill
-  \caption{Commands}
-  \label{fig:commands}
-\end{figure}
-
-
-\end{document}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
diff --git a/dev/doc/transition-V5.10-V6 b/dev/doc/transition-V5.10-V6
deleted file mode 100644
index df7b65dd8b..0000000000
--- a/dev/doc/transition-V5.10-V6
+++ /dev/null
@@ -1,5 +0,0 @@
-The V5.10 archive has been created with cvs in February 1995 by
-Jean-Christophe Filliâtre. It was moved to archive V6 in March 1996.
-At this occasion, the contrib directory (user-contributions) were
-moved to a separate directory and some theories (like ALGEBRA) moved
-to the user-contributions directory too.
diff --git a/dev/doc/transition-V6-V7 b/dev/doc/transition-V6-V7
deleted file mode 100644
index e477c9ff9d..0000000000
--- a/dev/doc/transition-V6-V7
+++ /dev/null
@@ -1,8 +0,0 @@
-The V6 archive has been created in March 1996 with files from the
-former V5.10 archive and has been abandoned in 2000.
-
-A new archive named V7 has been created in August 1999 by
-Jean-Christophe Filliâtre with a new architecture placing the
-type-checking at the kernel of Coq. This new architecture came with a
-"cleaner" organization of files, a uniform indentation style, uniform
-headers, etc.
diff --git a/dev/doc/translate.txt b/dev/doc/translate.txt
deleted file mode 100644
index 5b372c96c3..0000000000
--- a/dev/doc/translate.txt
+++ /dev/null
@@ -1,495 +0,0 @@
-
-                 How to use the translator
-                 =========================
-
-       (temporary version to be included in the official
-           TeX document describing the translator)
-
-The translator is a smart, robust and powerful tool to improve the
-readibility of your script. The current document describes the
-possibilities of the translator.
-
-In case of problem recompiling the translated files, don't waste time
-to modify the translated file by hand, read first the following
-document telling on how to modify the original files to get a smooth
-uniform safe translation. All 60000 lines of Coq lines on our
-user-contributions server have been translated without any change
-afterwards, and 0,5 % of the lines of the original files (mainly
-notations) had to be modified beforehand to get this result.
-
-Table of contents
------------------
-
-I) Implicit Arguments
- 1) Strict Implicit Arguments 
- 2) Implicit Arguments in standard library
-
-II) Notations
- 1) Translating a V7 notation as it was
- 2) Translating a V7 notation which conflicts with the new syntax
-  a) Associativity conflicts
-  b) Conflicts with other notations
-   b1) A notation hides another notation 
-   b2) A notation conflicts with the V8 grammar
-   b3) My notation is already defined at another level
-  c) How to use V8only with Distfix ?
-  d) Can I overload a notation in V8, e.g. use "*" and "+" ?
- 3) Using the translator to have simplest notations
- 4) Setting the translator to automatically use new notations that
-    wasn't used in old syntax
- 5) Defining a construction and its notation simultaneously
-
-III) Various pitfalls
- 1) New keywords
- 2) Old "Case" and "Match"
- 3) Change of definition or theorem names
- 4) Change of tactic names
-
----------------------------------------------------------------------
-
-I) Implicit Arguments
-   ------------------
-
-1) Strict Implicit Arguments 
-
-  "Set Implicit Arguments" changes its meaning in V8: the default is
-to turn implicit only the arguments that are _strictly_ implicit (or
-rigid), i.e. that remains inferable whatever the other arguments
-are. E.g "x" inferable from "P x" is not strictly inferable since it
-can disappears if "P" is instanciated by a term which erase "x".
-
-  To respect the old semantics, the default behaviour of the
-translator is to replace each occurrence "Set Implicit Arguments" by
-
-  Set Implicit Arguments.
-  Unset Strict Implicits.
-
-  However, you may wish to adopt the new semantics of "Set Implicit
-Arguments" (for instance because you think that the choice of
-arguments it setsimplicit is more "natural" for you). In this case,
-add the option -strict-implicit to the translator.
-
-  Warning: Changing the number of implicit arguments can break the
-notations.  Then use the V8only modifier of Notations.
-
-2) Implicit Arguments in standard library
-
-  Main definitions of standard library have now implicit
-arguments. These arguments are dropped in the translated files. This
-can exceptionally be a source of incompatibilities which has to be
-solved by hand (it typically happens for polymorphic functions applied
-to "nil" or "None").
-
-II) Notations
-    ---------
-
-  Grammar (on constr) and Syntax are no longer supported. Replace them by
-Notation before translation.
-
-  Precedence levels are now from 0 to 200. In V8, the precedence and
-associativity of an operator cannot be redefined. Typical level are
-(refer to the chapter on notations in the Reference Manual for the
-full list):
-
-  <-> : 95                    (no associativity)
-  -> : 90                     (right associativity)
-  \/ : 85                     (right associativity)
-  /\ : 80                     (right associativity)
-  ~ : 75                      (right associativity)
-  =, <, >, <=, >=, <> : 70    (no associativity)
-  +, - : 50                   (left associativity)
-  *, / : 40                   (left associativity)
-  ^ : 30                      (right associativity)
-
-1) Translating a V7 notation as it was
-
-  By default, the translator keeps the associativity given in V7 while
-the levels are mapped according to the following table:
- 
-  the V7 levels             [  0;  1;  2;  3;  4;  5;  6;  7;  8;  9;  10]
-  are resp. mapped in V8 to [  0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100]
-  with predefined assoc     [ No;  L;  R;  L;  L; No;  R;  R;  R; No;   L]
-
-  If this is OK for you, just simply apply the translator.
-
-2) Translating a V7 notation which conflicts with the new syntax
-
-a) Associativity conflict
-
-  Since the associativity of the levels obtained by translating a V7
-level (as shown on table above) cannot be changed, you have to choose
-another level with a compatible associativity.
-
-  You can choose any level between 0 and 200, knowing that the
-standard operators are already set at the levels shown on the list
-above. 
-
-Example 1: Assume you have a notation
-
-Infix NONA 2 "=_S" my_setoid_eq.
-
-By default, the translator moves it to level 30 which is right
-associative, hence a conflict with the expected no associativity.
-
-To solve the problem, just add the "V8only" modifier to reset the
-level and enforce the associativity as follows:
-
-Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity).
-
-The translator now knows that it has to translate "=_S" at level 70
-with no associativity.
-
-Rem: 70 is the "natural" level for relations, hence the choice of 70
-here, but any other level accepting a no-associativity would have been
-OK.
-
-Example 2: Assume you have a notation
-
-Infix RIGHTA 1 "o" my_comp.
-
-By default, the translator moves it to level 20 which is left
-associative, hence a conflict with the expected right associativity.
-
-To solve the problem, just add the "V8only" modifier to reset the
-level and enforce the associativity as follows:
-
-Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity).
-
-The translator now knows that it has to translate "o" at level 20
-which has the correct "right associativity".
-
-Rem: We assumed here that the user wants a strong precedence for
-composition, in such a way, say, that "f o g + h" is parsed as
-"(f o g) + h". To get "o" binding less than the arithmetical operators,
-an appropriated level would have been close of 70, and below, e.g. 65.
-
-b) Conflicts with other notations
-
-Since the new syntax comes with new keywords and new predefined
-symbols, new conflicts can occur. Again, you can use the option V8only
-to inform the translator of the new syntax to use.
-
-b1) A notation hides another notation 
-
-Rem: use Print Grammar constr in V8 to diagnose the overlap and see the
-section on factorization in the chapter on notations of the Reference
-Manual for hints on how to factorize.
-
-Example:
-
-Notation "{ x }" := (my_embedding x) (at level 1).
-
-overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at
-level 99. The conflicts can be solved by left-factorizing the notation
-as follows:
-
-Notation "{ x }" := (my_embedding x) (at level 1)
-  V8only (at level 0, x at level 99).
-
-b2) A notation conflicts with the V8 grammar.
-
-Again, use the V8only modifier to tell the translator to automatically
-take in charge the new syntax.
-
-Example:
-
-Infix 3 "@" app.
-
-Since "@" is used in the new syntax for deactivating the implicit
-arguments, another symbol has to be used, e.g. "@@". This is done via
-the V8only option as follows:
-
-Infix 3 "@" app V8only "@@" (at level 40, left associativity).
-
-or, alternatively by
-
-Notation "x @ y" := (app x y) (at level 3, left associativity)
-  V8only "x @@ y" (at level 40, left associativity).
-
-b3) My notation is already defined at another level (or with another
-associativity)
-
-In V8, the level and associativity of a given notation can no longer
-be changed. Then, either you adopt the standard reserved levels and
-associativity for this notation (as given on the list above) or you
-change your notation.
-
-- To change the notation, follow the directions in section b2.
-
-- To adopt the standard level, just use V8only without any argument.
-
-Example.
-
-Infix 6 "*" my_mult.
-
-is not accepted as such in V8. Write
-
-Infix 6 "*" my_mult V8only.
-
-to tell the translator to use "*" at the reserved level (i.e. 40 with
-left associativity). Even better, use interpretation scopes (look at
-the Reference Manual).
-
-c) How to use V8only with Distfix ?
-
-You can't, use Notation instead of Distfix.
-
-d) Can I overload a notation in V8, e.g. use "*" and "+" for my own
-algebraic operations ?
-
-Yes, using interpretation scopes (see the corresponding chapter in the
-Reference Manual).
-
-3) Using the translator to have simplest notations
-
-Thanks to the new syntax, * has now the expected left associativity,
-and the symbols <, >, <= and >= are now available.
-
-Thanks to the interpretation scopes, you can overload the
-interpretation of these operators with the default interpretation
-provided in Coq.
-
-This may be a motivation to use the translator to automatically change
-the notations while switching to the new syntax.
-
-See sections b) and d) above for examples.
-
-4) Setting the translator to automatically use new notations that
-wasn't used in old syntax
-
-Thanks to the "Notation" mechanism, defining symbolic notations is
-simpler than in the previous versions of Coq.
-
-Thanks to the new syntax and interpretation scopes, new symbols and
-overloading is available.
-
-This may be a motivation for using the translator to automatically change
-the notations while switching to the new syntax.
-
-Use for that the commands V8Notation and V8Infix.
-
-Examples:
-
-V8Infix "==>" my_relation (at level 65, right associativity).
-
-tells the translator to write an infix "==>" instead of my_relation in
-the translated files.
-
-V8Infix ">=" my_ge.
-
-tells the translator to write an infix ">=" instead of my_ge in the
-translated files and that the level and associativity are the standard
-one (as defined in the chart above).
-
-V8Infix ">=" my_ge : my_scope.
-
-tells the translator to write an infix ">=" instead of my_ge in the
-translated files, that the level and associativity are the standard
-one (as defined in the chart above), but only if scope my_scope is
-open or if a delimiting key is available for "my_scope" (see the
-Reference Manual).
-
-5) Defining a construction and its notation simultaneously
-
-This is permitted by the new syntax. Look at the Reference Manual for
-explanation. The translator is not fully able to take this in charge...
-
-III) Various pitfalls
-    ----------------
-
-1) New keywords
-
-  The following identifiers are new keywords
-
-  "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then";
-  "else"; "return"; "mod"; "at"; "let"; "_"; ".("
-
-  The translator automatically add a "_" to names clashing with a
-keyword, except for files. Hence users may need to rename the files
-whose name clashes with a keyword.
-
-  Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type"
-  were already keywords
-
-2) Old "Case" and "Match"
-
-  "Case" and "Match" are normally automatically translated into
-  "match" or "match" and "fix", but sometimes it fails to do so. It
-  typically fails when the Case or Match is argument of a tactic whose
-  typing context is unknown because of a preceding Intro/Intros, as e.g. in 
-
-     Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
-
-  The solution is then to replace the invocation of the sequence of
-  tactics into several invocation of the elementary tactics as follows
-
-     Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
-          ^^^
-
-3) Change of definition or theorem names
-
-  Type "entier" from fast_integer.v is renamed into "N" by the
-translator. As a consequence, user-defined objects of same name "N"
-are systematically qualified even tough it may not be necessary.  The
-same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST
-TO GIVE].
-
-4) Change of tactics names
-
-  Since tactics names are now lowercase, this can clash with
-user-defined tactic definitions. To pally this, clashing names are
-renamed by adding an extra "_" to their name.
-
-======================================================================
-Main examples for new syntax
-----------------------------
-
-1) Constructions
-
-  Applicative terms don't any longer require to be surrounded by parentheses as
-e.g in
-
-  "x = f y -> S x = S (f y)"
-
-
-  Product is written
-
-     "forall x y : T, U"
-     "forall x y, U"
-     "forall (x y : T) z (v w : V), U"
-     etc.
-
-  Abstraction is written
-
-     "fun x y : T, U"
-     "fun x y, U"
-     "fun (x y : T) z (v w : V), U"
-     etc.
-
-  Pattern-matching is written
-
-     "match x with c1 x1 x2 => t | c2 y as z => u end"
-     "match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end"
-     "match v1 as y in le _ n, v2 as z in I p q return P n y p q z with
-         c1 x1 x2, _ => t | c2 y, d z => u end"
-
-     The last example is the new form of what was written
-
-    "<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of
-         (c1 x1 x2) _ => t | (c2 y) (d z) => u end"
-
-  Pattern-matching of type with one constructors and no dependencies
-of the arguments in the resulting type can be written
-
-    "let (x,y,z) as u return P u := t in v"
-     
-  Local fixpoints are written
-
-    "fix f (n m:nat) z (x : X) {struct m} : nat := ...
-     with ..."
-
-    and "struct" tells which argument is structurally decreasing.
-
-  Explicitation of implicit arguments is written
-
-     "f @1:=u v @3:=w t"
-     "@f u v w t"
-
-2) Tactics
-
-  The main change is that tactics names are now lowercase. Besides
-this, the following renaming are applied:
-
-  "NewDestruct" -> "destruct"
-  "NewInduction" -> "induction"
-  "Induction" -> "simple induction"
-  "Destruct" -> "simple destruct"
-
-  For tactics with occurrences, the occurrences now comes after and
-  repeated use is separated by comma as in
-
-  "Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4"
-  "Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4"
-  "Simpl 1 3 e" -> "simpl e at 1 3"
-
-3) Tactic language
-
-  Definitions are now introduced with keyword "Ltac" (instead of
-"Tactic"/"Meta" "Definition") and are implicitly recursive
-("Recursive" is no longer used).
-
-  The new rule for distinguishing terms from ltac expressions is:
-
-  Write "ltac:" in front of any tactic in argument position and
-  "constr:" in front of any construction in head position
-
-4) Vernacular language
-
-a) Assumptions
-
-  The syntax for commands is mainly unchanged. Declaration of
-assumptions is now done as follows
-
-  Variable m : t.
-  Variables m n p : t.
-  Variables (m n : t) (u v : s) (w : r).
-  
-b) Definitions
-
-  Definitions are done as follows
-
-  Definition f m n : t := ... .
-  Definition f m n := ... .
-  Definition f m n := ... : t.
-  Definition f (m n : u) : t := ... .
-  Definition f (m n : u) := ... : t.
-  Definition f (m n : u) := ... .
-  Definition f a b (p q : v) r s (m n : t) : t := ... .
-  Definition f a b (p q : v) r s (m n : t) := ... .
-  Definition f a b (p q : v) r s (m n : t) := ... : t.
-
-c) Fixpoints
-
-  Fixpoints are done this way
-  
-  Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... .
-  Fixpoint f x : v := ... .
-  Fixpoint f (x : t) : v := ... .
-
-  It is possible to give a concrete notation to a fixpoint as follows
-
-  Fixpoint plus (n m:nat) {struct n} : nat as "n + m" :=
-    match n with
-    | O => m
-    | S p => S (p + m)
-    end.
-
-d) Inductive types
-
-  The syntax for inductive types is as follows
-
-  Inductive t (a b : u) (d : e) : v :=
-     c1 : w1 | c2 : w2 | ... .
-
-  Inductive t (a b : u) (d : e) : v :=
-     c1 : w1 | c2 : w2 | ... .
-
-  Inductive t (a b : u) (d : e) : v :=
-     c1 (x y : t) : w1 | c2 (z : r) : w2 | ... .
-
-  As seen in the last example, arguments of the constructors can be
-given before the colon. If the type itself is omitted (allowed only in
-case the inductive type has no real arguments), this yields an
-ML-style notation as follows
-
-  Inductive nat : Set := O | S (n:nat).
-  Inductive bool : Set := true | false.
-
-  It is even possible to define a syntax at the same time, as follows:
-
-  Inductive or (A B:Prop) : Prop as "A \/ B":=
-    | or_introl (a:A) : A \/ B 
-    | or_intror (b:B) : A \/ B.
-
-  Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B).
-