Merge PR #819: Cleanup old things

14 files changed, 62 insertions, 456 deletions

diff --git a/dev/README b/dev/README
index 814f609576..b446c3e974 100644
--- a/dev/README
+++ b/dev/README
@@ -40,10 +40,6 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html)
 Other development tools (directory tools)
 -----------------------
 
-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
 anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse
   location of Anomaly backtraces and jump to them conveniently from
diff --git a/dev/TODO b/dev/TODO
deleted file mode 100644
index e62ee6e537..0000000000
--- a/dev/TODO
+++ /dev/null
@@ -1,22 +0,0 @@
-
- o options de la ligne de commande
-     - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml
-
- o arguments implicites
-     - les calculer une fois pour toutes à la déclaration (dans Declare)
-       et stocker cette information dans le in_variable, in_constant, etc.
-
- o Environnements compilés (type Environ.compiled_env)
-     - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?)
-
- o Efficacité
-     - utiliser DOPL plutôt que DOPN (sauf pour Case)
-     - batch mode => pas de undo, ni de reset
-     - conversion : déplier la constante la plus récente
-     - un cache pour type_of_const, type_of_inductive, type_of_constructor,
-       lookup_mind_specif
-
- o Toplevel
-     - parsing de la ligne de commande : utiliser Arg ???
-
-
diff --git a/dev/db_printers.ml b/dev/db_printers.ml
deleted file mode 100644
index f4b4a425e2..0000000000
--- a/dev/db_printers.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-open Pp
-open Names
-
-let pp s = pp (hov 0 s)
-
-let prid id = Format.print_string (Id.to_string id)
-let prsp sp = Format.print_string (DirPath.to_string sp)
-
-
diff --git a/dev/doc/api.txt b/dev/doc/api.txt
deleted file mode 100644
index 5827257b53..0000000000
--- a/dev/doc/api.txt
+++ /dev/null
@@ -1,10 +0,0 @@
-Recommendations in using the API:
-
-The type of terms: constr (see kernel/constr.ml and kernel/term.ml)
-
-- On type constr, the canonical equality on CIC (up to
-  alpha-conversion and cast removal) is Constr.equal
-- The type constr is abstract, use mkRel, mkSort, etc. to build
-  elements in constr; use "kind_of_term" to analyze the head of a
-  constr; use destRel, destSort, etc. when the head constructor is
-  known
diff --git a/dev/doc/notes-on-conversion b/dev/doc/notes-on-conversion.v
index a81f170c63..a81f170c63 100644
--- a/dev/doc/notes-on-conversion
+++ b/dev/doc/notes-on-conversion.v
diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel
deleted file mode 100644
index ffdb1bdca9..0000000000
--- a/dev/tools/Makefile.devel
+++ /dev/null
@@ -1,74 +0,0 @@
-# to be linked to makefile (lowercase - takes precedence over Makefile)
-# in main directory
-# make devel in main directory should do this for you.
-
-TOPDIR=.
-BASEDIR=
-
-SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API
-
-default:	usage noargument
-
-usage::
-	@echo Usage: make \<target\>
-	@echo Targets are:
-
-usage::
-	@echo "  setup-devel	-- set the devel makefile"
-setup-devel:
-	@ln -sfv dev/tools/Makefile.devel makefile
-	@(for i in $(SOURCEDIRS); do \
-	    (cd $(TOPDIR)/$$i; ln -sfv ../dev/tools/Makefile.dir Makefile) \
-	done)
-
-
-usage::
-	@echo "  clean-devel	-- clear all devel files"
-clean-devel:
-	echo rm -f makefile .depend.devel
-	echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile)
-
-
-usage::
-	@echo "  coqtop	-- make until the bytecode executable, make the link"
-coqtop:	bin/coqtop.byte
-	ln -sf bin/coqtop.byte coqtop
-
-
-usage::
-	@echo "  quick		-- make bytecode executable and states"
-quick: 
-	$(MAKE) states BEST=byte
-
-include Makefile
-
-include $(TOPDIR)/dev/tools/Makefile.common
-
-# this file is better described in dev/tools/Makefile.dir
-include .depend.devel
-
-#if dev/tools/Makefile.local exists, it is included
-ifneq ($(wildcard $(TOPDIR)/dev/tools/Makefile.local),)
-include $(TOPDIR)/dev/tools/Makefile.local
-endif
-
-
-usage::
-	@echo "  total		-- runs coqtop with all theories required"
-total:
-	ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th))))
-
-
-usage::
-	@echo "  run		-- makes and runs bytecode coqtop using ledit and the history file"
-	@echo "		   if you want to pass arguments to coqtop, use make run ARG=<args>"
-run:	$(TOPDIR)/coqtop
-	ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS)
-
-
-usage::
-	@echo "  vars		-- echos commands to set COQTOP and COQBIN variables"
-vars:
-	@(cd $(TOPDIR); \
-	echo export COQTOP=`pwd`/ ; \
-	echo export COQBIN=`pwd`/bin/ )
diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir
deleted file mode 100644
index 1a1bb90b44..0000000000
--- a/dev/tools/Makefile.dir
+++ /dev/null
@@ -1,131 +0,0 @@
-# make a link to this file if you are working hard in one directory of Coq
-#   ln -s ../dev/tools/Makefile.dir Makefile
-# if you are working in a sub/dir/ make a link to dev/tools/Makefile.subdir instead
-# this Makefile provides many useful facilities to develop Coq
-# it is not completely compatible with .ml4 files unfortunately
-
-ifndef TOPDIR
-TOPDIR=..
-endif
-
-# this complicated thing should work for subsubdirs as well
-BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||"))
-
-noargs:	dir
-
-test-dir:
-	@echo TOPDIR=$(TOPDIR)
-	@echo BASEDIR=$(BASEDIR)
-
-include $(TOPDIR)/dev/tools/Makefile.common
-
-# make this directory
-dir:
-	$(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR))
-
-# make all cmo's in this directory. Useful in case the main Makefile is not
-# up-to-date
-all:	
-	@( ( for i in *.ml; do \
-	       echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \
-	     done; \
-	     for i in *.ml4; do \
-	       echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \
-	     done ) \
-	  | xargs $(MAKE) -C $(TOPDIR) )
-
-# lists all files that should be compiled in this directory
-list:
-	@(for i in *.mli; do \
-	   ls -l `basename $$i .mli`.cmi; \
-	done)
-	@(for i in *.ml; do \
-	   ls -l `basename $$i .ml`.cmo; \
-	done)
-	@(for i in *.ml4; do \
-	   ls -l `basename $$i .ml4`.cmo; \
-	done)
-
-
-clean::  
-	rm -f *.cmi *.cmo *.cmx *.o
-
-
-# if grammar.cmo files cannot be compiled and main .depend cannot be
-# rebuilt, this is quite useful
-depend:
-	(cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel)
-
-
-# displays the dependency graph of the current directory (vertically,
-# unlike in doc/)
-graph:
-	(ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) &
-
-
-# the pretty entry draws a dependency graph marking red those nodes
-# which do not have their .cmo files 
-
-.INTERMEDIATE: depend.dot depend.2.dot
-.PHONY: depend.ps
-
-depend.dot:
-	ocamldep *.ml *.mli | ocamldot > $@
-
-depend.2.dot:	depend.dot
-	(i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@
-	(for ml in *.ml; do \
-	   base=`basename $$ml .ml`; \
-	   fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \
-	   rest=`echo $$base | cut -c2-`; \
-	   name=`echo $$fst $$rest | tr -d " "`; \
-	   cmo=$$base.cmo; \
-	   if [ ! -e $$cmo ]; then \
-	     echo \"$$name\" [color=red]\; >> $@;\
-	   fi;\
-         done;\
-	 echo } >> $@)
-
-depend.ps:	depend.2.dot
-	dot -Tps $< > $@
-
-clean::
-	rm -f depend.ps
-
-pretty:	depend.ps
-	(gv -spartan $<; rm $<) &
-#	gv -spartan $< &
-
-
-
-# generating file.ml.mli by tricking make to pass -i to ocamlc 
-
-%.ml.mli:	FORCE
-	@(cmo=`basename $@ .ml.mli`.cmo ; \
-	mv -f $$cmo $$cmo.tmp ; \
-	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \
-	echo Generated interface file $@ ; \
-	mv -f $$cmo.tmp $$cmo)
-
-%.annot:	FORCE
-	@(cmo=`basename $@ .annot`.cmo ; \
-	mv -f $$cmo $$cmo.tmp ; \
-	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \
-	echo Generated annotation file $@ ; \
-	mv -f $$cmo.tmp $$cmo)
-
-FORCE:
-
-clean::
-	rm -f *.ml.mli
-
-# this is not perfect but mostly WORKS! It just calls the main makefile
-
-%.cmi:	FORCE
-	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
-
-%.cmo:	FORCE
-	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
-
-coqtop:	
-	$(MAKE) -C $(TOPDIR) bin/coqtop.byte
diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir
deleted file mode 100644
index cb914bd129..0000000000
--- a/dev/tools/Makefile.subdir
+++ /dev/null
@@ -1,7 +0,0 @@
-# if you work in a sub/sub-rectory of Coq
-# you should make a link to that makefile 
-#    ln -s ../../dev/tools/Makefile.subdir Makefile
-# in order to have all the facilities of dev/tools/Makefile.dir
-
-TOPDIR=../..
-include $(TOPDIR)/dev/tools/Makefile.dir
diff --git a/dev/v8-syntax/.gitignore b/dev/v8-syntax/.gitignore
new file mode 100644
index 0000000000..89e3509b00
--- /dev/null
+++ b/dev/v8-syntax/.gitignore
@@ -0,0 +1,6 @@
+# byproducts of check-grammar
+def
+df
+use
+use-k
+use-t
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index fa2864cec9..6b7960c92f 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -1158,7 +1158,7 @@ $$
 \nlsep \TERM{Abort}~\NT{ident}
 \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body}
 \nlsep \TERM{Qed}
-\nlsep \TERM{Save}~\NT{ident}}
+\nlsep \TERM{Save}~\NT{ident}
 \nlsep \TERM{Defined}~\OPT{\NT{ident}}
 \nlsep \TERM{Suspend}
 \nlsep \TERM{Resume}~\OPT{\NT{ident}}
diff --git a/doc/Makefile.rt b/doc/Makefile.rt
deleted file mode 100644
index 6c32813462..0000000000
--- 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 8cfeebc28b..4b0ab31254 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 ac1686c25e..0000000000
--- 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 aefea8d429..0000000000
--- 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}