Merge PR #819: Cleanup old things

4 files changed, 55 insertions, 191 deletions

diff --git a/doc/Makefile.rt b/doc/Makefile.rt
deleted file mode 100644
index 6c3281346..000000000
--- a/doc/Makefile.rt
+++ /dev/null
@@ -1,43 +0,0 @@
-# Makefile for building Coq Technical Reports
-
-# if coqc,coqtop,coq-tex are not in your PATH, you need the environment 
-# variable COQBIN to be correctly set  
-# (COQTOP is autodetected)
-# (some files are preprocessed using Coq and some part of the documentation
-# is automatically built from the theories sources)
-
-# To compile documentation, you need the following tools:
-# Dvi: latex (latex2e), bibtex, makeindex, dviselect (package RPM dviutils)
-# Ps: dvips, psutils (ftp://ftp.dcs.ed.ac.uk/pub/ajcd/psutils.tar.gz)
-# Pdf: pdflatex
-# Html:
-#   - hevea: http://para.inria.fr/~maranget/hevea/
-#   - htmlSplit: http://coq.inria.fr/~delahaye
-# Rapports INRIA: dviselect, rrkit (par Michel Mauny)
-
-include ./Makefile
-
-###################
-# RT
-###################
-# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny)
-rt/Reference-Manual-RT.dvi: refman/Reference-Manual.dvi rt/RefMan-cover.tex
-	dviselect -i refman/Reference-Manual.dvi -o rt/RefMan-body.dvi 3:
-	(cd rt; $(LATEX) RefMan-cover.tex)
-	set a=`tail -1 refman/Reference-Manual.log`;\
-	set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\
-	(cd rt; if $(TEST) "$$a = 0";\
-	 then rrkit  RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\
-	 else rrkit -odd RefMan-cover.dvi RefMan-body.dvi Reference-Manual-RT.dvi;\
-	fi)
-
-# Fabrication d'un RT INRIA (utilise rrkit de Michel Mauny)
-rt/Tutorial-RT.dvi : tutorial/Tutorial.v.dvi rt/Tutorial-cover.tex
-	dviselect -i rt/Tutorial.v.dvi -o rt/Tutorial-body.dvi 3:
-	(cd rt; $(LATEX) Tutorial-cover.tex)
-	set a=`tail -1 tutorial/Tutorial.v.log`;\
-	set a=expr \("$$a" : '.*(\(.*\) pages.*'\) % 2;\
-	(cd rt; if $(TEST) "$$a = 0";\
-	 then rrkit      Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\
-	 else rrkit -odd Tutorial-cover.dvi Tutorial-body.dvi Tutorial-RT.dvi;\
-	fi)
diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v
index 8cfeebc28..4b0ab3125 100644
--- a/doc/RecTutorial/RecTutorial.v
+++ b/doc/RecTutorial/RecTutorial.v
@@ -1,3 +1,5 @@
+Unset Automatic Introduction.
+
 Check (forall A:Type, (exists x:A, forall (y:A), x <> y) -> 2 = 3).
 
 
@@ -69,13 +71,13 @@ Check (Prop::Set::nil).
 
 Require Import Bvector.
 
-Print vector.
+Print Vector.t.
 
-Check (Vnil nat).
+Check (Vector.nil nat).
 
-Check (fun (A:Type)(a:A)=> Vcons _ a _ (Vnil _)).
+Check (fun (A:Type)(a:A)=> Vector.cons _ a _ (Vector.nil _)).
 
-Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
+Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))).
 
 Lemma eq_3_3 : 2 + 1 = 3.
 Proof.
@@ -146,6 +148,7 @@ Proof.
  intros; absurd (p < p); eauto with arith.
 Qed.
 
+Require Extraction.
 Extraction max.
 
 
@@ -300,8 +303,8 @@ Section Le_case_analysis.
            (HS : forall m, n <= m -> Q (S m)).
  Check (
     match H in (_ <= q) return (Q q)  with
-    | le_n => H0
-    | le_S m Hm => HS m Hm
+    | le_n _ => H0
+    | le_S _ m Hm => HS m Hm
     end
   ).
 
@@ -317,16 +320,16 @@ Proof.
 Qed.
 
 Definition Vtail_total
-   (A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
-match v in (vector _ n0) return (vector A (pred n0)) with
-| Vnil => Vnil A
-| Vcons _ n0 v0 => v0
+   (A : Type) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):=
+match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with
+| Vector.nil _ => Vector.nil A
+| Vector.cons _ _ n0 v0 => v0
 end.
 
-Definition Vtail' (A:Type)(n:nat)(v:vector A n) : vector A (pred n).
+Definition Vtail' (A:Type)(n:nat)(v:Vector.t A n) : Vector.t A (pred n).
  intros A n v; case v.
  simpl.
- exact (Vnil A).
+ exact (Vector.nil A).
  simpl.
  auto.
 Defined.
@@ -498,10 +501,8 @@ Inductive  typ : Type :=
 
 Definition typ_inject: typ.
 split.
-exact typ.
+Fail exact typ.
 (*
-Defined.
-
 Error: Universe Inconsistency.
 *)
 Abort.
@@ -920,7 +921,6 @@ Defined.
 Print minus_decrease.
 
 
-
 Definition div_aux (x y:nat)(H: Acc lt x):nat.
  fix 3.
  intros.
@@ -969,40 +969,40 @@ let rec div_aux x y =
            | Right -> div_aux (minus x y) y)
 *)
 
-Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A.
 Proof.
  intros A v;inversion v.
 Abort.
 
 (*
- Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n),
-                                  n= 0 -> v = Vnil A.
+ Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n),
+                                  n= 0 -> v = Vector.nil A.
 
 Toplevel input, characters 40281-40287
-> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),                                    n= 0 -> v = Vnil A.
+> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),                                    n= 0 -> v = Vector.nil A.
 >                                                                                                                 ^^^^^^
 Error: In environment
 A : Set
 n : nat
-v : vector A n
+v : Vector.t A n
 e : n = 0
-The term "Vnil A" has type "vector A 0" while it is expected to have type
- "vector A n"
+The term "Vector.nil A" has type "Vector.t A 0" while it is expected to have type
+ "Vector.t A n"
 *)
  Require Import JMeq.
 
 
 (* On devrait changer Set en Type ? *)
 
-Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n),
-                                  n= 0 -> JMeq v (Vnil A).
+Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:Vector.t A n),
+                                  n= 0 -> JMeq v (Vector.nil A).
 Proof.
  destruct v.
  auto.
  intro; discriminate.
 Qed.
 
-Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Type)(v:Vector.t A 0), v = Vector.nil A.
 Proof.
  intros a v;apply JMeq_eq.
  apply vector0_is_vnil_aux.
@@ -1010,56 +1010,56 @@ Proof.
 Qed.
 
 
-Implicit Arguments Vcons [A n].
-Implicit Arguments Vnil [A].
-Implicit Arguments Vhead [A n].
-Implicit Arguments Vtail [A n].
+Implicit Arguments Vector.cons [A n].
+Implicit Arguments Vector.nil [A].
+Implicit Arguments Vector.hd [A n].
+Implicit Arguments Vector.tl [A n].
 
-Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
+Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n.
 Proof.
  destruct n; intro v.
- exact Vnil.
- exact (Vcons  (Vhead v) (Vtail v)).
+ exact Vector.nil.
+ exact (Vector.cons  (Vector.hd v) (Vector.tl v)).
 Defined.
 
-Eval simpl in (fun (A:Type)(v:vector A 0) => (Vid _ _ v)).
+Eval simpl in (fun (A:Type)(v:Vector.t A 0) => (Vid _ _ v)).
 
-Eval simpl in (fun (A:Type)(v:vector A 0) => v).
+Eval simpl in (fun (A:Type)(v:Vector.t A 0) => v).
 
 
 
-Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v).
 Proof.
  destruct v.
  reflexivity.
  reflexivity.
 Defined.
 
-Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
+Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil.
 Proof.
  intros.
- change (Vnil (A:=A)) with (Vid _ 0 v).
+ change (Vector.nil (A:=A)) with (Vid _ 0 v).
  apply Vid_eq.
 Defined.
 
 
 Theorem decomp :
-  forall (A : Type) (n : nat) (v : vector A (S n)),
-  v = Vcons (Vhead v) (Vtail v).
+  forall (A : Type) (n : nat) (v : Vector.t A (S n)),
+  v = Vector.cons (Vector.hd v) (Vector.tl v).
 Proof.
  intros.
- change (Vcons (Vhead v) (Vtail v)) with (Vid _  (S n) v).
+ change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _  (S n) v).
  apply Vid_eq.
 Defined.
 
 
 
 Definition vector_double_rect :
-    forall (A:Type) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
-        P 0 Vnil Vnil ->
-        (forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
-             P (S n) (Vcons a v1) (Vcons  b v2)) ->
-        forall n (v1 v2 : vector A n), P n v1 v2.
+    forall (A:Type) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type),
+        P 0 Vector.nil Vector.nil ->
+        (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 ->
+             P (S n) (Vector.cons a v1) (Vector.cons  b v2)) ->
+        forall n (v1 v2 : Vector.t A n), P n v1 v2.
  induction n.
  intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
  auto.
@@ -1069,24 +1069,23 @@ Defined.
 
 Require Import Bool.
 
-Definition bitwise_or n v1 v2 : vector bool n :=
-   vector_double_rect bool  (fun n v1 v2 => vector bool n)
-                        Vnil
-                        (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
-
+Definition bitwise_or n v1 v2 : Vector.t bool n :=
+   vector_double_rect bool  (fun n v1 v2 => Vector.t bool n)
+                        Vector.nil
+                        (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2.
 
-Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p){struct v}
+Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:Vector.t A p){struct v}
                   : option A :=
   match n,v  with
-    _   , Vnil => None
-  | 0   , Vcons b  _ _ => Some b
-  | S n', Vcons _  p' v' => vector_nth A n'  p' v'
+    _   , Vector.nil => None
+  | 0   , Vector.cons b  _ => Some b
+  | S n', @Vector.cons _  _ p' v' => vector_nth A n' p' v'
   end.
 
 Implicit Arguments vector_nth [A p].
 
 
-Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i  a b,
+Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i  a b,
       vector_nth i v1 = Some a ->
       vector_nth i v2 = Some b ->
       vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
diff --git a/doc/rt/RefMan-cover.tex b/doc/rt/RefMan-cover.tex
deleted file mode 100644
index ac1686c25..000000000
--- a/doc/rt/RefMan-cover.tex
+++ /dev/null
@@ -1,45 +0,0 @@
-\documentstyle[RRcover]{book}
-        % The use of the style `french' forces the french abstract to appear first.
-
-\RRtitle{Manuel de r\'ef\'erence du syst\`eme Coq \\ version V7.1}
-\RRetitle{The Coq Proof Assistant \\ Reference Manual \\ Version 7.1
-\thanks
-{This research was partly supported by ESPRIT Basic Research
-Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.}
-}
-\RRauthor{Bruno Barras, Samuel Boutin, Cristina Cornes,
-Judica\"el Courant, Jean-Christophe Filli\^atre, Eduardo Gim\'enez,
-Hugo Herbelin, G\'erard Huet, C\'esar Mu\~noz, Chetan Murthy,
-Catherine Parent, Christine Paulin-Mohring,
-Amokrane Sa{\"\i}bi, Benjamin Werner}
-\authorhead{}
-\titlehead{Coq V7.1 Reference Manual}
-\RRtheme{2}
-\RRprojet{Coq}
-\RRNo{0123456789}
-\RRdate{May 1997}
-%\RRpages{}
-\URRocq
-
-\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la
-v\'erification de preuves formelles dans une logique d'ordre
-sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
-Ce document constitue le manuel de r\'ef\'erence de la version V7.1
-qui est distribu\'ee par ftp anonyme \`a l'adresse
-\url{ftp://ftp.inria.fr/INRIA/coq/}}
-
-\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles,
-Calcul des Constructions Inductives}
-
-
-\RRabstract{Coq is a proof assistant based on a higher-order logic
-allowing powerful definitions of functions. 
-Coq V7.1 is available by anonymous
-ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}}
-
-\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives
-Constructions}
-
-\begin{document}
-\makeRT
-\end{document}
diff --git a/doc/rt/Tutorial-cover.tex b/doc/rt/Tutorial-cover.tex
deleted file mode 100644
index aefea8d42..000000000
--- a/doc/rt/Tutorial-cover.tex
+++ /dev/null
@@ -1,47 +0,0 @@
-\documentstyle[RRcover]{book}
-        % The use of the style `french' forces the french abstract to appear first.
-\RRetitle{
-The Coq Proof Assistant \\ A Tutorial \\ Version 7.1
-\thanks{This research was partly supported by ESPRIT Basic Research
-Action ``Types'' and by the GDR ``Programmation'' co-financed by MRE-PRC and CNRS.}
-}
-\RRtitle{Coq \\ Une introduction \\ V7.1 }
-\RRauthor{G\'erard Huet, Gilles Kahn and Christine Paulin-Mohring}
-\RRtheme{2}
-\RRprojet{{Coq
-\\[15pt]
-{INRIA Rocquencourt}
-{\hskip -5.25pt}
-~~{\bf ---}~~
- \def\thefootnote{\arabic{footnote}\hss}
-{CNRS - ENS Lyon}
-\footnote[1]{LIP URA 1398 du CNRS,
-46 All\'ee d'Italie, 69364 Lyon CEDEX 07, France.}
-{\hskip -14pt}}}
-
-%\RRNo{0123456789}
-\RRNo{0204}
-\RRdate{Ao\^ut 1997}
-
-\URRocq
-\RRresume{Coq est un syst\`eme permettant le d\'eveloppement et la
-v\'erification de preuves formelles dans une logique d'ordre
-sup\'erieure incluant un riche langage de d\'efinitions de fonctions.
-Ce document constitue une introduction pratique \`a l'utilisation de
-la version V7.1 qui est distribu\'ee par ftp anonyme \`a l'adresse
-\url{ftp://ftp.inria.fr/INRIA/coq/}}
-
-\RRmotcle{Coq, Syst\`eme d'aide \`a la preuve, Preuves formelles, Calcul
-des Constructions Inductives}
-
-\RRabstract{Coq is a proof assistant based on a higher-order logic
-allowing powerful definitions of functions. This document is a
-tutorial for the version V7.1 of Coq. This version is available by
-anonymous ftp at \url{ftp://ftp.inria.fr/INRIA/coq/}}
-
-\RRkeyword{Coq, Proof Assistant, Formal Proofs, Calculus of Inductives
-Constructions}
-
-\begin{document}
-\makeRT
-\end{document}