First release of Vector library.

To avoid names&notations clashs with list, Vector shouldn't be
"Import"ed but one can "Import Vector.VectorNotations." to have
notations.

SetoidVector at least remains to do.

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

47 files changed, 792 insertions, 314 deletions

diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index 08a090325..f384e1488 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -34,4 +34,4 @@ Definition nat_noteq_bool x y :=
   bool_of_sumbool (sumbool_not _ _ (eq_nat_dec x y)).
 
 Definition zerop_bool x := bool_of_sumbool (zerop x).
-Definition notzerop_bool x := bool_of_sumbool (notzerop x).
\ No newline at end of file
+Definition notzerop_bool x := bool_of_sumbool (notzerop x).
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index c6bf35bb0..c9e6d3cf3 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -50,4 +50,4 @@ Qed.
 
 Require Export Wf_nat.
 
-Require Export Min Max.
\ No newline at end of file
+Require Export Min Max.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 2b2cf860d..bcfbe0efe 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -39,4 +39,4 @@ Definition min_glb := Nat.min_glb.
 (* Compatibility *)
 Notation min_case2 := min_case (only parsing).
 Notation min_SS := Nat.succ_min_distr (only parsing).
-(* end hide *)
\ No newline at end of file
+(* end hide *)
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 9e3823d7a..6eb667c11 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -7,7 +7,8 @@
 (************************************************************************)
 
 Require Import Decidable.
-
+Require Eqdep_dec.
+Require Import Le Lt.
 Open Local Scope nat_scope.
 
 Implicit Types m n x y : nat.
@@ -30,3 +31,22 @@ Hint Resolve O_or_S eq_nat_dec: arith.
 Theorem dec_eq_nat : forall n m, decidable (n = m).
   intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith.
 Defined.
+
+Definition UIP_nat:= Eqdep_dec.UIP_dec eq_nat_dec.
+
+Lemma le_unique: forall m n (h1 h2: m <= n), h1 = h2.
+Proof.
+fix 3.
+refine (fun m _ h1 => match h1 as h' in _ <= k return forall hh: m <= k, h' = hh
+  with le_n => _ |le_S i H => _ end).
+refine (fun hh => match hh as h' in _ <= k return forall eq: m = k, 
+  le_n m = match eq in _ = p return m <= p -> m <= m with |eq_refl => fun bli => bli end h' with
+    |le_n => fun eq => _ |le_S j H' => fun eq => _ end eq_refl).
+rewrite (UIP_nat _ _ eq eq_refl). reflexivity.
+subst m. destruct (Lt.lt_irrefl j H').
+refine (fun hh => match hh as h' in _ <= k return match k as k' return m <= k' -> Prop
+  with |0 => fun _ => True |S i' => fun h'' => forall H':m <= i', le_S m i' H' = h'' end h'
+    with |le_n => _ |le_S j H2 => fun H' => _ end H).
+destruct m. exact I. intros; destruct (Lt.lt_irrefl m H').
+f_equal. apply le_unique.
+Qed.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 48d730319..eb2d4df4c 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -24,17 +24,10 @@ Open Local Scope nat_scope.
 
 Implicit Types m n p q : nat.
 
-(** * Zero is neutral *)
-
-Lemma plus_0_l : forall n, 0 + n = n.
-Proof.
-  reflexivity.
-Qed.
-
-Lemma plus_0_r : forall n, n + 0 = n.
-Proof.
-  intro; symmetry  in |- *; apply plus_n_O.
-Qed.
+(** * Zero is neutral 
+Deprecated : Already in Init/Peano.v *)
+Definition plus_0_l n := eq_sym (plus_O_n n).
+Definition plus_0_r n := eq_sym (plus_n_O n).
 
 (** * Commutativity *)
 
@@ -47,14 +40,8 @@ Hint Immediate plus_comm: arith v62.
 
 (** * Associativity *)
 
-Lemma plus_Snm_nSm : forall n m, S n + m = n + S m.
-Proof.
-  intros.
-  simpl in |- *.
-  rewrite (plus_comm n m).
-  rewrite (plus_comm n (S m)).
-  trivial with arith.
-Qed.
+Definition plus_Snm_nSm : forall n m, S n + m = n + S m:=
+ plus_n_Sm.
 
 Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p.
 Proof.
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 694ed15b4..0c2181638 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -9,6 +9,8 @@
 (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
 
 Require Export Bool Sumbool.
+Require Vector.
+Export Vector.VectorNotations.
 Require Import Minus.
 
 Open Local Scope nat_scope.
@@ -27,161 +29,6 @@ as definition, since the type inference mechanism for pattern-matching
 is sometimes weaker that the one implemented for elimination tactiques.
 *)
 
-Section VECTORS.
-
-(**
-A vector is a list of size n whose elements belongs to a set A.
-If the size is non-zero, we can extract the first component and the
-rest of the vector, as well as the last component, or adding or
-removing a component (carry) or repeating the last component at the
-end of the vector.
-We can also truncate the vector and remove its p last components or
-reciprocally extend the vector by concatenation.
-A unary function over A generates a function on vectors of size n by
-applying f pointwise.
-A binary function over A generates a function on pairs of vectors of
-size n by applying f pointwise.
-*)
-
-Variable A : Type.
-
-Inductive vector : nat -> Type :=
-  | Vnil : vector 0
-  | Vcons : forall (a:A) (n:nat), vector n -> vector (S n).
-
-Definition Vhead (n:nat) (v:vector (S n)) :=
-  match v with
-  | Vcons a _ _ => a
-  end.
-
-Definition Vtail (n:nat) (v:vector (S n)) :=
-  match v with
-  | Vcons _ _ v => v
-  end.
-
-Definition Vlast : forall n:nat, vector (S n) -> A.
-Proof.
-  induction n as [| n f]; intro v.
-  inversion v.
-  exact a.
-
-  inversion v as [| n0 a H0 H1].
-  exact (f H0).
-Defined.
-
-Fixpoint Vconst (a:A) (n:nat) :=
-  match n return vector n with
-  | O => Vnil
-  | S n => Vcons a _ (Vconst a n)
-  end.
-
-(** Shifting and truncating *)
-
-Lemma Vshiftout : forall n:nat, vector (S n) -> vector n.
-Proof.
-  induction n as [| n f]; intro v.
-  exact Vnil.
-
-  inversion v as [| a n0 H0 H1].
-  exact (Vcons a n (f H0)).
-Defined.
-
-Lemma Vshiftin : forall n:nat, A -> vector n -> vector (S n).
-Proof.
-  induction n as [| n f]; intros a v.
-  exact (Vcons a 0 v).
-
-  inversion v as [| a0 n0 H0 H1 ].
-  exact (Vcons a0 (S n) (f a H0)).
-Defined.
-
-Lemma Vshiftrepeat : forall n:nat, vector (S n) -> vector (S (S n)).
-Proof.
-  induction n as [| n f]; intro v.
-  inversion v.
-  exact (Vcons a 1 v).
-
-  inversion v as [| a n0 H0 H1 ].
-  exact (Vcons a (S (S n)) (f H0)).
-Defined.
-
-Lemma Vtrunc : forall n p:nat, n > p -> vector n -> vector (n - p).
-Proof.
-  induction p as [| p f]; intros H v.
-  rewrite <- minus_n_O.
-  exact v.
-
-  apply (Vshiftout (n - S p)).
-
-  rewrite minus_Sn_m.
-  apply f.
-  auto with *.
-  exact v.
-  auto with *.
-Defined.
-
-(** Concatenation of two vectors *)
-
-Fixpoint Vextend n p (v:vector n) (w:vector p) : vector (n+p) :=
-  match v with
-  | Vnil => w
-  | Vcons a n' v' => Vcons a (n'+p) (Vextend n' p v' w)
-  end.
-
-(** Uniform application on the arguments of the vector *)
-
-Variable f : A -> A.
-
-Fixpoint Vunary n (v:vector n) : vector n :=
-  match v with
-  | Vnil => Vnil
-  | Vcons a n' v' => Vcons (f a) n' (Vunary n' v')
-  end.
-
-Variable g : A -> A -> A.
-
-Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n.
-Proof.
-  induction n as [| n h]; intros v v0.
-  exact Vnil.
-
-  inversion v as [| a n0 H0 H1]; inversion v0 as [| a0 n1 H2 H3].
-  exact (Vcons (g a a0) n (h H0 H2)).
-Defined.
-
-(** Eta-expansion of a vector *)
-
-Definition Vid n : vector n -> vector n :=
-  match n with
-  | O => fun _ => Vnil
-  | _ => fun v => Vcons (Vhead _ v) _ (Vtail _ v)
-  end.
-
-Lemma Vid_eq : forall (n:nat) (v:vector n), v = Vid n v.
-Proof.
-  destruct v; auto.
-Qed.
-
-Lemma VSn_eq :
-  forall (n : nat) (v : vector (S n)), v = Vcons (Vhead _ v) _ (Vtail _ v).
-Proof.
-  intros.
-  exact (Vid_eq _ v).
-Qed.
-
-Lemma V0_eq : forall (v : vector 0), v = Vnil.
-Proof.
-  intros.
-  exact (Vid_eq _ v).
-Qed.
-
-End VECTORS.
-
-(* suppressed: incompatible with Coq-Art book
-Implicit Arguments Vnil [A].
-Implicit Arguments Vcons [A n].
-*)
-
 Section BOOLEAN_VECTORS.
 
 (**
@@ -197,38 +44,38 @@ NOTA BENE: all shift operations expect predecessor of size as parameter
 (they only work on non-empty vectors).
 *)
 
-Definition Bvector := vector bool.
+Definition Bvector := Vector.t bool.
 
-Definition Bnil := @Vnil bool.
+Definition Bnil := @Vector.nil bool.
 
-Definition Bcons := @Vcons bool.
+Definition Bcons := @Vector.cons bool.
 
-Definition Bvect_true := Vconst bool true.
+Definition Bvect_true := Vector.const true.
 
-Definition Bvect_false := Vconst bool false.
+Definition Bvect_false := Vector.const false.
 
-Definition Blow := Vhead bool.
+Definition Blow := @Vector.hd bool.
 
-Definition Bhigh := Vtail bool.
+Definition Bhigh := @Vector.tl bool.
 
-Definition Bsign := Vlast bool.
+Definition Bsign := @Vector.last bool.
 
-Definition Bneg := Vunary bool negb.
+Definition Bneg n (v : Bvector n) := Vector.map negb v.
 
-Definition BVand := Vbinary bool andb.
+Definition BVand n (v : Bvector n) := Vector.map2 andb v.
 
-Definition BVor := Vbinary bool orb.
+Definition BVor n (v : Bvector n) := Vector.map2 orb v.
 
-Definition BVxor := Vbinary bool xorb.
+Definition BVxor n (v : Bvector n) := Vector.map2 xorb v.
 
 Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
-  Bcons carry n (Vshiftout bool n bv).
+  Bcons carry n (Vector.shiftout bv).
 
 Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
-  Bhigh (S n) (Vshiftin bool (S n) carry bv).
+  Bhigh (S n) (Vector.shiftin carry bv).
 
 Definition BshiftRa (n:nat) (bv:Bvector (S n)) :=
-  Bhigh (S n) (Vshiftrepeat bool n bv).
+  Bhigh (S n) (Vector.shiftrepeat bv).
 
 Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   match p with
@@ -250,5 +97,3 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
 
 End BOOLEAN_VECTORS.
 
-Implicit Arguments Vcons [[A] [n]] [].
-Implicit Arguments Vnil [[A]] [].
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 6550a4955..6872eaea3 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -45,4 +45,4 @@ Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}.
 destruct b; intro H.
 left; inversion H; auto with bool.
 right; inversion H; auto with bool.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 942607faf..73a092143 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -66,4 +66,4 @@ Definition bool_of_sumbool :
   intros A B H.
   elim H; intro; [exists true | exists false]; assumption.
 Defined.
-Implicit Arguments bool_of_sumbool.
\ No newline at end of file
+Implicit Arguments bool_of_sumbool.
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index a7c739625..bac4c0d69 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -37,4 +37,4 @@ Hint Resolve zerob_false_intro: bool.
 Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
 Proof.
   destruct n; [ inversion 1 | auto with bool ].
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 2b7fe88bf..a001f2e92 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -34,4 +34,4 @@ Ltac unconvertible :=
     | |- _ => exact tt
   end.
 
-Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
\ No newline at end of file
+Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index f449d8383..216ca35af 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -50,13 +50,7 @@ Qed.
 
 (** Injectivity of successor *)
 
-Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
-Proof.
-  intros n m Sn_eq_Sm.
-  replace (n=m) with (pred (S n) = pred (S m)) by auto using pred_Sn.
-  rewrite Sn_eq_Sm; trivial.
-Qed.
-
+Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H.
 Hint Immediate eq_add_S: core.
 
 Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v
index ff9ec7f69..f0876fbcd 100644
--- a/theories/Logic/SetIsType.v
+++ b/theories/Logic/SetIsType.v
@@ -14,4 +14,4 @@
     Set: simply insert some Require Export of this file at starting
     points of the development and try to recompile...  *)
 
-Notation "'Set'" := Type (only parsing).
\ No newline at end of file
+Notation "'Set'" := Type (only parsing).
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 0dd2fceaa..5b3157143 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -710,7 +710,8 @@ Lemma Nneg_bit0 :
    Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a').
 Proof.
   intros.
-  rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false.
+  rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, 
+    xorb_nilpotent, xorb_false.
   reflexivity.
 Qed.
 
@@ -733,7 +734,8 @@ Lemma Nsame_bit0 :
 Proof.
   intros. rewrite <- (xorb_false (Nbit0 a)).
   assert (H0: Nbit0 (Npos (xO p)) = false) by reflexivity.
-  rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. reflexivity.
+  rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb.
+    reflexivity.
 Qed.
 
 (** a lexicographic order on bits, starting from the lowest bit *)
@@ -840,8 +842,8 @@ Lemma Nless_trans :
    Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true.
 Proof.
   induction a as [|a IHa|a IHa] using N_ind_double; intros a' a'' H H0.
-    destruct (Nless N0 a'') as []_eqn:Heqb. trivial.
-     rewrite (N0_less_2 a'' Heqb), (Nless_z a') in H0. discriminate H0.
+    case_eq (Nless N0 a'') ; intros Heqn. trivial.
+     rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0.
     induction a' as [|a' _|a' _] using N_ind_double.
       rewrite (Nless_z (Ndouble a)) in H. discriminate H.
       rewrite (Nless_def_1 a a') in H.
@@ -868,10 +870,10 @@ Lemma Nless_total :
  forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.
 Proof.
   induction a using N_rec_double; intro a'.
-    destruct (Nless N0 a') as []_eqn:Heqb. left. left. auto.
+    case_eq (Nless N0 a') ; intros Heqb. left. left. auto.
      right. rewrite (N0_less_2 a' Heqb). reflexivity.
     induction a' as [|a' _|a' _] using N_rec_double.
-      destruct (Nless N0 (Ndouble a)) as []_eqn:Heqb. left. right. auto.
+      case_eq (Nless N0 (Ndouble a)) ; intros Heqb. left. right. auto.
        right. exact (N0_less_2 _  Heqb).
       rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->].
         left. assumption.
@@ -910,9 +912,9 @@ Definition N2Bv (n:N) : Bvector (Nsize n) :=
 
 Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
   match bv with
-    | Vnil => N0
-    | Vcons false n bv => Ndouble (Bv2N n bv)
-    | Vcons true n bv => Ndouble_plus_one (Bv2N n bv)
+    | Vector.nil => N0
+    | Vector.cons false n bv => Ndouble (Bv2N n bv)
+    | Vector.cons true n bv => Ndouble_plus_one (Bv2N n bv)
   end.
 
 Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.
@@ -928,13 +930,12 @@ Qed.
 
 Lemma Bv2N_Nsize : forall n (bv:Bvector n), Nsize (Bv2N n bv) <= n.
 Proof.
-induction n; intros.
-rewrite (V0_eq _ bv); simpl; auto.
-rewrite (VSn_eq _ _ bv); simpl.
-specialize IHn with (Vtail _ _ bv).
-destruct (Vhead _ _ bv);
- destruct (Bv2N n (Vtail bool n bv));
-  simpl; auto with arith.
+induction bv; intros.
+auto.
+simpl.
+destruct h;
+ destruct (Bv2N n bv);
+ simpl ; auto with arith.
 Qed.
 
 (** In the previous lemma, we can only replace the inequality by
@@ -944,15 +945,10 @@ Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)),
   Bsign _ bv = true <->
   Nsize (Bv2N _ bv) = (S n).
 Proof.
-induction n; intro.
-rewrite (VSn_eq _ _ bv); simpl.
-rewrite (V0_eq _ (Vtail _ _ bv)); simpl.
-destruct (Vhead _ _ bv); simpl; intuition; try discriminate.
-rewrite (VSn_eq _ _ bv); simpl.
-generalize (IHn (Vtail _ _ bv)); clear IHn.
-destruct (Vhead _ _ bv);
- destruct (Bv2N (S n) (Vtail bool (S n) bv));
-  simpl; intuition; try discriminate.
+apply Vector.rectS ; intros ; simpl.
+destruct a ; compute ; split ; intros x ; now inversion x.
+ destruct a, (Bv2N (S n) v) ;
+  simpl ;intuition ; try discriminate.
 Qed.
 
 (** To state nonetheless a second result about composition of
@@ -982,7 +978,7 @@ Qed.
    [a] plus some zeros. *)
 
 Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat),
- N2Bv_gen (Nsize a + k) a = Vextend _ _ _ (N2Bv a) (Bvect_false k).
+ N2Bv_gen (Nsize a + k) a = Vector.append (N2Bv a) (Bvect_false k).
 Proof.
 destruct a; simpl.
 destruct k; simpl; auto.
@@ -994,13 +990,13 @@ Qed.
 Lemma N2Bv_Bv2N : forall n (bv:Bvector n),
    N2Bv_gen n (Bv2N n bv) = bv.
 Proof.
-induction n; intros.
-rewrite (V0_eq _ bv); simpl; auto.
-rewrite (VSn_eq _ _ bv); simpl.
-generalize (IHn (Vtail _ _ bv)); clear IHn.
+induction bv; intros.
+auto.
+simpl.
+generalize IHbv; clear IHbv.
 unfold Bcons.
-destruct (Bv2N _ (Vtail _ _ bv));
- destruct (Vhead _ _ bv); intro H; rewrite <- H; simpl; trivial;
+destruct (Bv2N _ bv);
+ destruct h; intro H; rewrite <- H; simpl; trivial;
   induction n; simpl; auto.
 Qed.
 
@@ -1009,31 +1005,25 @@ Qed.
 Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)),
   Nbit0 (Bv2N _ bv) = Blow _ bv.
 Proof.
+apply Vector.caseS.
 intros.
 unfold Blow.
-rewrite (VSn_eq _ _ bv) at 1.
 simpl.
-destruct (Bv2N n (Vtail bool n bv)); simpl;
- destruct (Vhead bool n bv); auto.
+destruct (Bv2N n t); simpl;
+ destruct h; auto.
 Qed.
 
-Definition Bnth (n:nat)(bv:Bvector n)(p:nat) : p<n -> bool.
-Proof.
- induction bv in p |- *.
- intros.
- exfalso; inversion H.
- intros.
- destruct p.
- exact a.
- apply (IHbv p); auto with arith.
-Defined.
+Notation Bnth := (@Vector.nth_order bool).
 
 Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n),
-  Bnth _ bv p H = Nbit (Bv2N _ bv) p.
+  Bnth bv H = Nbit (Bv2N _ bv) p.
 Proof.
 induction bv; intros.
 inversion H.
-destruct p; simpl; destruct (Bv2N n bv); destruct a; simpl in *; auto.
+destruct p ; simpl.
+  destruct (Bv2N n bv); destruct h; simpl in *; auto.
+  specialize IHbv with p (lt_S_n _ _ H).
+    simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto.
 Qed.
 
 Lemma Nbit_Nsize : forall n p, Nsize n <= p -> Nbit n p = false.
@@ -1045,12 +1035,12 @@ inversion H.
 inversion H.
 Qed.
 
-Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth _ (N2Bv n) p H.
+Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth (N2Bv n) H.
 Proof.
 destruct n as [|n].
 inversion H.
-induction n; simpl in *; intros; destruct p; auto with arith.
-inversion H; inversion H1.
+induction n ; destruct p ; unfold Vector.nth_order in *; simpl in * ; auto.
+intros H ; destruct (lt_n_O _ (lt_S_n _ _ H)).
 Qed.
 
 (** Binary bitwise operations are the same in the two worlds. *)
@@ -1058,35 +1048,17 @@ Qed.
 Lemma Nxor_BVxor : forall n (bv bv' : Bvector n),
   Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv').
 Proof.
-induction n; intros bv bv'.
-rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto.
-rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto.
-rewrite IHn.
-destruct (Vhead bool n bv), (Vhead bool n bv'),
- (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv'));
- simpl; auto.
-Qed.
-
-Lemma Nor_BVor : forall n (bv bv' : Bvector n),
-  Bv2N _ (BVor _ bv bv') = Nor (Bv2N _ bv) (Bv2N _ bv').
-Proof.
-induction n; intros bv bv'.
-rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto.
-rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto.
-rewrite IHn.
-destruct (Vhead bool n bv), (Vhead bool n bv'),
- (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv'));
- simpl; auto.
+apply Vector.rect2 ; intros.
+now simpl.
+simpl.
+destruct a, b, (Bv2N n v1), (Bv2N n v2); simpl in *; rewrite H ; now simpl.
 Qed.
 
 Lemma Nand_BVand : forall n (bv bv' : Bvector n),
   Bv2N _ (BVand _ bv bv') = Nand (Bv2N _ bv) (Bv2N _ bv').
 Proof.
-induction n; intros bv bv'.
-rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto.
-rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto.
-rewrite IHn.
-destruct (Vhead bool n bv), (Vhead bool n bv'),
- (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv'));
+refine (Vector.rect2 _ _ _); simpl; intros; auto.
+rewrite H.
+destruct a, b, (Bv2N n v1), (Bv2N n v2);
  simpl; auto.
 Qed.
diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v
index 9d399f5cd..22adc5050 100644
--- a/theories/NArith/Ndist.v
+++ b/theories/NArith/Ndist.v
@@ -333,4 +333,4 @@ Proof.
   intro. rewrite <- H. apply Nplength_ultra.
   rewrite Nxor_assoc. rewrite <- (Nxor_assoc a'' a'' a'). rewrite Nxor_nilpotent.
   rewrite Nxor_neutral_left. reflexivity.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 43aafe24b..20016281a 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -413,4 +413,4 @@ Qed.
 Lemma eqb_correct : forall x y, eqb x y = true -> x==y.
 Proof. now apply eqb_eq. Qed.
 
-End CyclicRing.
\ No newline at end of file
+End CyclicRing.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index a5b537caa..1acdd17e5 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1692,7 +1692,7 @@ Section Int31_Specs.
  unfold head031, recl.
  change On with (phi_inv (Z_of_nat (31-size))).
  replace (head031_alt size x) with
-   (head031_alt size x + (31 - size))%nat by (apply plus_0_r; auto).
+   (head031_alt size x + (31 - size))%nat by auto.
  assert (size <= 31)%nat by auto with arith.
 
  revert x H; induction size; intros.
@@ -1800,7 +1800,7 @@ Section Int31_Specs.
  unfold tail031, recr.
  change On with (phi_inv (Z_of_nat (31-size))).
  replace (tail031_alt size x) with
-   (tail031_alt size x + (31 - size))%nat by (apply plus_0_r; auto).
+   (tail031_alt size x + (31 - size))%nat by auto.
  assert (size <= 31)%nat by auto with arith.
 
  revert x H; induction size; intros.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index 788ca8e56..9981fab71 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -128,4 +128,4 @@ Module Type ZType_Notation (Import Z:ZType).
  Infix "<" := lt.
 End ZType_Notation.
 
-Module Type ZType' := ZType <+ ZType_Notation.
\ No newline at end of file
+Module Type ZType' := ZType <+ ZType_Notation.
diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v
index de40f0704..2bdc1bba2 100644
--- a/theories/Numbers/Rational/SpecViaQ/QSig.v
+++ b/theories/Numbers/Rational/SpecViaQ/QSig.v
@@ -220,4 +220,4 @@ End QProperties.
 
 Module QTypeExt (Q : QType)
  <: QType <: TotalOrder <: HasCompare Q <: HasMinMax Q <: HasEqBool Q
- := Q <+ QProperties.
\ No newline at end of file
+ := Q <+ QProperties.
diff --git a/theories/PArith/Pminmax.v b/theories/PArith/Pminmax.v
index 6fe6435a0..10eaa1608 100644
--- a/theories/PArith/Pminmax.v
+++ b/theories/PArith/Pminmax.v
@@ -123,4 +123,4 @@ Proof.
  apply plus_min_distr_l.
 Qed.
 
-End P.
\ No newline at end of file
+End P.
diff --git a/theories/Program/Program.v b/theories/Program/Program.v
index 8d7185828..14a7ffca7 100644
--- a/theories/Program/Program.v
+++ b/theories/Program/Program.v
@@ -11,4 +11,4 @@ Require Export Coq.Program.Equality.
 Require Export Coq.Program.Subset.
 Require Export Coq.Program.Basics.
 Require Export Coq.Program.Combinators.
-Require Export Coq.Program.Syntax.
\ No newline at end of file
+Require Export Coq.Program.Syntax.
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 1e1fcf935..d8176dc25 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -53,4 +53,4 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *)
 (* Extract Inductive sigT => "prod" [ "" ]. *)
-*)
\ No newline at end of file
+*)
diff --git a/theories/QArith/Qminmax.v b/theories/QArith/Qminmax.v
index 01c6ab678..2da24ee6b 100644
--- a/theories/QArith/Qminmax.v
+++ b/theories/QArith/Qminmax.v
@@ -64,4 +64,4 @@ Proof.
  apply plus_min_distr_l.
 Qed.
 
-End Q.
\ No newline at end of file
+End Q.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 601c2549e..24f6d7204 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -208,4 +208,4 @@ intro; apply H; apply eqR_Qeq.
 rewrite H0; unfold Q2R in |- *; simpl in |- *; field; auto with real.
 Qed.
 
-End LegacyQField.
\ No newline at end of file
+End LegacyQField.
diff --git a/theories/Reals/Integration.v b/theories/Reals/Integration.v
index 2c69350d3..da1742ca6 100644
--- a/theories/Reals/Integration.v
+++ b/theories/Reals/Integration.v
@@ -8,4 +8,4 @@
 
 Require Export NewtonInt.
 Require Export RiemannInt_SF.
-Require Export RiemannInt.
\ No newline at end of file
+Require Export RiemannInt.
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index 28d4a37cb..a15e9949d 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -27,4 +27,4 @@ Require Export Rfunctions.
 Require Export SeqSeries.
 Require Export Rtrigo.
 Require Export Ranalysis.
-Require Export Integration.
\ No newline at end of file
+Require Export Integration.
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 65bf76c5f..5f8b5d9da 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -133,7 +133,7 @@ Section sequence.
     clear -Hi2pn.
     intros m.
     induction n.
-    rewrite plus_0_r.
+    rewrite<- plus_n_O.
     ring_simplify (sum m + (/ 2) ^ m - (/ 2) ^ m).
     split ; apply Rle_refl.
     rewrite <- plus_n_Sm.
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index dfd029d96..d612e71ec 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -105,4 +105,4 @@ Section Specific_orders.
     {PO_of_chain : PO U;
     Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
 
-End Specific_orders.
\ No newline at end of file
+End Specific_orders.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index 0907d689b..24facb6f6 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -200,4 +200,4 @@ Section Image.
 
 End Image.
 
-Hint Resolve Im_def image_empty finite_image: sets v62.
\ No newline at end of file
+Hint Resolve Im_def image_empty finite_image: sets v62.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index f13ffd51a..a319b9832 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -97,4 +97,4 @@ Section Partial_order_facts.
     apply Strict_Rel_Transitive_with_Rel with (y := y);
       [ intuition | unfold Strict_Rel_of in H', H'0; intuition ].
   Qed.
-End Partial_order_facts.
\ No newline at end of file
+End Partial_order_facts.
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 49c97251f..e28a12644 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -84,4 +84,4 @@ Section Axiomatisation.
     apply cong_left; apply perm_left.
   Qed.
 
-End Axiomatisation.
\ No newline at end of file
+End Axiomatisation.
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 8742d4c37..f8b24e747 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -185,4 +185,4 @@ Hint Resolve Union_increases_r: sets v62.
 Hint Resolve Intersection_decreases_l: sets v62.
 Hint Resolve Intersection_decreases_r: sets v62.
 Hint Resolve Empty_set_is_Bottom: sets v62.
-Hint Resolve Strict_inclusion_is_transitive: sets v62.
\ No newline at end of file
+Hint Resolve Strict_inclusion_is_transitive: sets v62.
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 9cfe37e59..a7fbb53da 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -62,4 +62,4 @@ End Relations_1.
 Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
   same_relation: sets v62.
 Hint Resolve Definition_of_preorder Definition_of_order
-  Definition_of_equivalence Definition_of_PER: sets v62.
\ No newline at end of file
+  Definition_of_equivalence Definition_of_PER: sets v62.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index 05e2fb80d..0c8329dd0 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -107,4 +107,4 @@ intros U R R' H' H'0; red in |- *.
 elim H'.
 intros H'1 H'2 x y z H'3 H'4; apply H'2.
 apply H'0 with y; auto with sets.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 8b4a20ff9..e7a69c99e 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -51,4 +51,4 @@ End Relations_2.
 Hint Resolve Rstar_0: sets v62.
 Hint Resolve Rstar1_0: sets v62.
 Hint Resolve Rstar1_1: sets v62.
-Hint Resolve Rplus_0: sets v62.
\ No newline at end of file
+Hint Resolve Rplus_0: sets v62.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 13ec1e6c4..89b98c1f5 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -148,4 +148,4 @@ elim (H'3 t); auto with sets.
 intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5.
 exists z1; split; [ idtac | assumption ].
 apply Rstar_n with t; auto with sets.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index f48b9761e..8ac6e7fb4 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -166,4 +166,4 @@ generalize (H'2 v); intro h; lapply h;
 red in |- *; (exists z1; split); auto with sets.
 apply T with y1; auto with sets.
 apply T with t; auto with sets.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 119fcf803..bf1aaf8db 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -210,4 +210,4 @@ i*)
 
 End defs.
 
-Unset Implicit Arguments.
\ No newline at end of file
+Unset Implicit Arguments.
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
new file mode 100644
index 000000000..b90937a40
--- /dev/null
+++ b/theories/Vectors/Fin.v
@@ -0,0 +1,190 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+Require Arith_base.
+
+(** [fin n] is a convinient way to represent \[1 .. n\]
+
+[fin n] can be seen as a n-uplet of unit where [F1] is the first element of
+the n-uplet and [FS] set (n-1)-uplet of all the element but the first.
+
+   Author: Pierre Boutillier
+   Institution: PPS, INRIA 12/2010
+*)
+
+Inductive t : nat -> Set :=
+|F1 : forall {n}, t (S n)
+|FS : forall {n}, t n -> t (S n).
+
+Section SCHEMES.
+Definition case0 {P} (p: t 0): P p :=
+  match p as p' in t n return
+    match n as n' return t n' -> Type
+  with |0 => fun f0 => P f0 |S _ => fun _ => @ID end p'
+  with |F1 _ => @id |FS _ _ => @id end.
+
+Definition caseS (P: forall n, t (S n) -> Type)
+  (P1: forall n, P n F1) (PS : forall n (p: t n), P n (FS p))
+  n (p: t (S n)): P n p :=
+  match p as p0 in t n0
+  return match n0 as nn return t nn -> Type with
+    |0 => fun _ => @ID |S n' => fun p' => P n' p'
+  end p0 with
+  |F1 k => P1 k
+  |FS k pp => PS k pp
+  end.
+
+Definition rectS (P: forall n, t (S n) -> Type)
+  (P1: forall n, P n F1) (PS : forall n (p: t (S n)), P n p -> P (S n) (FS p)):
+  forall n (p: t (S n)), P n p :=
+fix rectS_fix n (p: t (S n)): P n p:=
+  match p as p0 in t n0
+  return match n0 as nn return t nn -> Type with
+    |0 => fun _ => @ID |S n' => fun p' => P n' p'
+  end p0 with
+  |F1 k => P1 k
+  |FS 0 pp => @case0 (fun f => P 0 (FS f)) pp
+  |FS (S k) pp => PS k pp (rectS_fix k pp)
+  end.
+
+Definition rect2 (P: forall {n} (a b: t n), Type)
+  (H0: forall n, P (S n) F1 F1)
+  (H1: forall n (f: t n), P (S n) F1 (FS f))
+  (H2: forall n (f: t n), P (S n) (FS f) F1)
+  (HS: forall n (f g : t n), P n f g -> P (S n) (FS f) (FS g)):
+    forall n (a b: t n), P n a b :=
+fix rect2_fix n (a: t n): forall (b: t n), P n a b :=
+match a with
+  |F1 m => fun (b: t (S m)) => match b as b' in t n'
+                   return match n' as n0
+                          return t n0 -> Type with
+                            |0 => fun _ => @ID
+                            |S n0 => fun b0 => P (S n0) F1 b0
+                          end b' with
+                     |F1 m' => H0 m'
+                     |FS m' b' => H1 m' b'
+                   end
+  |FS m a' => fun (b: t (S m)) => match b as b' in t n'
+                      return match n' as n0
+                             return t n0 -> Type with
+                               |0 => fun _ => @ID
+                               |S n0 => fun b0 =>
+                                 forall (a0: t n0), P (S n0) (FS a0) b0
+                             end b' with
+                         |F1 m' => fun aa => H2 m' aa
+                         |FS m' b' => fun aa => HS m' aa b' (rect2_fix m' aa b')
+                       end a'
+end.
+End SCHEMES.
+
+(** [to_nat f] = p iff [f] is the p{^ th} element of [fin m]. *)
+Fixpoint to_nat {m} (n : t m) : {i | i < m} :=
+  match n in t k return {i | i< k} with
+    |F1 j => exist (fun i => i< S j) 0 (Lt.lt_0_Sn j)
+    |FS _ p => match to_nat p with |exist i P => exist _ (S i) (Lt.lt_n_S _ _ P) end
+  end.
+
+(** [of_nat p n] answers the p{^ th} element of [fin n] if p < n or a proof of
+p >= n else *)
+Fixpoint of_nat (p n : nat) : (t n) + { exists m, p = n + m } :=
+  match n with
+   |0 => inright _ (ex_intro (fun x => p = 0 + x) p (@eq_refl _ p))
+   |S n' => match p with
+      |0 => inleft _ (F1)
+      |S p' => match of_nat p' n' with
+        |inleft f => inleft _ (FS f)
+        |inright arg => inright _ (match arg with |ex_intro m e =>
+          ex_intro (fun x => S p' = S n' + x) m (f_equal S e) end)
+      end
+    end
+  end.
+
+(** [of_nat_lt p n H] answers the p{^ th} element of [fin n]
+it behaves much better than [of_nat p n] on open term *)
+Fixpoint of_nat_lt {p n : nat} : p < n -> t n :=
+  match n with
+    |0 => fun H : p < 0 => False_rect _ (Lt.lt_n_O p H)
+    |S n' => match p with
+      |0 => fun _ => @F1 n'
+      |S p' => fun H => FS (of_nat_lt (Lt.lt_S_n _ _ H))
+    end
+  end.
+
+Lemma of_nat_to_nat_inv {m} (p : t m) : of_nat_lt (proj2_sig (to_nat p)) = p.
+Proof.
+induction p.
+ reflexivity.
+ simpl; destruct (to_nat p). simpl. subst p; repeat f_equal. apply Peano_dec.le_unique.
+Qed.
+
+(** [weak p f] answers a function witch is the identity for the p{^  th} first
+element of [fin (p + m)] and [FS (FS .. (FS (f k)))] for [FS (FS .. (FS k))]
+with p FSs *)
+Fixpoint weak {m}{n} p (f : t m -> t n) :
+  t (p + m) -> t (p + n) :=
+match p as p' return t (p' + m) -> t (p' + n) with
+  |0 => f
+  |S p' => fun x => match x in t n0 return
+     match n0 with |0 => @ID |S n0' => n0' = p' + m -> t (S p' + n) end with
+     |F1 n' => fun eq : n' = p' + m => F1
+     |FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq))
+  end (eq_refl _)
+end.
+
+(** The p{^ th} element of [fin m] viewed as the p{^ th} element of
+[fin (m + n)] *)
+Fixpoint L {m} n (p : t m) : t (m + n) :=
+  match p with |F1 _ => F1 |FS _ p' => FS (L n p') end.
+
+Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p).
+Proof.
+induction p.
+  reflexivity.
+  simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p).
+Qed.
+
+(** The p{^ th} element of [fin m] viewed as the p{^ th} element of
+[fin (n + m)]
+Really really ineficient !!! *)
+Definition L_R {m} n (p : t m) : t (n + m).
+induction n.
+  exact p.
+  exact ((fix LS k (p: t k) :=
+    match p in t n0 return t (S n0) with
+      |F1 _ => F1
+      |FS _ p' => FS (LS _ p')
+    end) _ IHn).
+Defined.
+
+(** The p{^ th} element of [fin m] viewed as the (n + p){^ th} element of
+[fin (n + m)] *)
+Fixpoint R {m} n (p : t m) : t (n + m) :=
+  match n with |0 => p |S n' => FS (R n' p) end.
+
+Lemma R_sanity {m} n (p : t m) : proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p).
+Proof.
+induction n.
+  reflexivity.
+  simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p).
+Qed.
+
+Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) :=
+match o with
+  |F1 m' => L (m' * n) p
+  |FS m' o' => R n (depair o' p)
+end.
+
+Lemma depair_sanity {m n} (o : t m) (p : t n) :
+  proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)).
+induction o ; simpl.
+  rewrite L_sanity. now rewrite Mult.mult_0_r.
+
+  rewrite R_sanity. rewrite IHo.
+  rewrite Plus.plus_assoc. destruct (to_nat o); simpl; rewrite Mult.mult_succ_r.
+    now rewrite (Plus.plus_comm n).
+Qed.
\ No newline at end of file
diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v
new file mode 100644
index 000000000..f3e5e338f
--- /dev/null
+++ b/theories/Vectors/Vector.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Vectors.
+
+   Author: Pierre Boutillier
+   Institution: PPS, INRIA 12/2010
+
+Originally from the contribution bit vector by Jean Duprat (ENS Lyon).
+
+Based on contents from Util/VecUtil of the CoLoR contribution *)
+
+Require Fin.
+Require VectorDef.
+Require VectorSpec.
+Include VectorDef.
+Include VectorSpec.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
new file mode 100644
index 000000000..e5bb66a20
--- /dev/null
+++ b/theories/Vectors/VectorDef.v
@@ -0,0 +1,330 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Definitions of Vectors and functions to use them
+
+   Author: Pierre Boutillier
+   Institution: PPS, INRIA 12/2010
+*)
+
+(**
+Names should be "caml name in list.ml" if exists and order of arguments
+have to be the same. complain if you see mistakes ... *)
+
+Require Import Arith_base.
+Require Fin.
+Open Local Scope nat_scope.
+
+(**
+A vector is a list of size n whose elements belong to a set A. *)
+
+Inductive t A : nat -> Type :=
+  |nil : t A 0
+  |cons : forall (h:A) (n:nat), t A n -> t A (S n).
+
+Local Notation "[]" := (nil _).
+Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity).
+
+Section SCHEMES.
+
+(** An induction scheme for non-empty vectors *)
+Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
+ (bas: forall a: A, P 0 (a :: []))
+ (rect: forall a {n} (v: t A (S n)), P n v -> P (S n) (a :: v)) :=
+ fix rectS_fix {n} (v: t A (S n)) : P n v :=
+ match v with
+ |nil => @id
+ |cons a 0 v =>
+     match v as vnn in t _ nn
+       return
+         match nn as nnn return t A nnn -> Type with
+         |0 => fun vm => P 0 (a :: vm)
+         |S _ => fun _ => ID
+         end vnn
+     with
+     |nil => bas a
+     |_ :: _ => @id
+     end
+ |cons a (S nn') v => rect a nn' v (rectS_fix _ v)
+ end.
+
+(** An induction scheme for 2 vectors of same length *)
+Definition rect2 {A B} (P:forall n, t A n -> t B n -> Type)
+  (bas : P 0 [] []) (rect : forall n v1 v2, P n v1 v2 ->
+    forall a b, P (S n) (a :: v1) (b :: v2)) :=
+fix rect2_fix {n} (v1:t A n):
+  forall v2 : t B n, P n v1 v2 :=
+match v1 as v1' in t _ n1
+  return forall v2 : t B n1, P n1 v1' v2 with
+  |[] => fun v2 =>
+     match v2 as v2' in t _ n2
+       return match n2 as n2' return t B n2' -> Type with
+         |0 => fun v2 => P 0 [] v2 |S _ => fun _ => @ID end v2' with
+       |[] => bas
+       |_ :: _ => @id
+     end
+  |h1 :: t1 => fun v2 =>
+    match v2 as v2' in t _ n2
+      return match n2 as n2'
+        return t B n2' -> Type with
+        |0 => fun _ => @ID
+        |S n' => fun v2 => forall t1' : t A n',
+          P (S n') (h1 :: t1') v2
+        end v2' with
+      |[] => @id
+      |h2 :: t2 => fun t1' =>
+        rect _ t1' t2 (rect2_fix _ t1' t2) h1 h2
+    end t1
+end.
+
+(** A vector of length [0] is [nil] *)
+Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v :=
+match v with
+  |[] => H
+end.
+
+(** A vector of length [S _] is [cons] *)
+Definition caseS {A} (P : forall n, t A (S n) -> Type)
+  (H : forall h n t, P _ (h :: t)) n v : P n v :=
+match v with
+  |[] => @id (* Why needed ? *)
+  |h :: t => H h _ t
+end.
+End SCHEMES.
+
+Section BASES.
+(** The first element of a non empty vector *)
+Definition hd {A} {n} (v:t A (S n)) := Eval cbv delta beta in
+(caseS (fun n v => A) (fun h n t => h) n v).
+
+(** The last element of an non empty vector *)
+Definition last {A} {n} (v : t A (S n)) := Eval cbv delta in
+(rectS (fun _ _ => A) (fun a => a) (fun _ _ _ H => H) _ v).
+
+(** Build a vector of n{^ th} [a] *)
+Fixpoint const {A} (a:A) (n:nat) :=
+  match n return t A n with
+  | O => nil A
+  | S n => a :: (const a n)
+  end.
+
+(** The [p]{^ th} element of a vector of length [m].
+
+Computational behavior of this function should be the same as
+ocaml function. *)
+Fixpoint nth {A} {m} (v' : t A m) (p : Fin.t m) {struct p} : A :=
+match p in Fin.t m' return t A m' -> A with
+ |Fin.F1 q => fun v => caseS (fun n v' => A) (fun h n t => h) q v
+ |Fin.FS q p' => fun v => (caseS (fun n v' => Fin.t n -> A)
+   (fun h n t p0 => nth t p0) q v) p'
+end v'.
+
+(** An equivalent definition of [nth]. *)
+Definition nth_order {A} {n} (v: t A n) {p} (H: p < n) :=
+(nth v (Fin.of_nat_lt H)).
+
+(** Put [a] at the p{^ th} place of [v] *)
+Fixpoint replace {A n} (v : t A n) (p: Fin.t n) (a : A) {struct p}: t A n :=
+  match p in Fin.t j return t A j -> t A j with
+  |Fin.F1 k => fun v': t A (S k) => caseS (fun n _ => t A (S n)) (fun h _ t => a :: t) _ v'
+  |Fin.FS k p' => fun v': t A (S k) =>
+    (caseS (fun n _ => Fin.t n -> t A (S n)) (fun h _ t p2 => h :: (replace t p2 a)) _ v') p'
+  end v.
+
+(** Version of replace with [lt] *)
+Definition replace_order {A n} (v: t A n) {p} (H: p < n) :=
+replace v (Fin.of_nat_lt H).
+
+(** Remove the first element of a non empty vector *)
+Definition tl {A} {n} (v:t A (S n)) := Eval cbv delta beta in
+(caseS (fun n v => t A n) (fun h n t => t) n v).
+
+(** Remove last element of a non-empty vector *)
+Definition shiftout {A} {n:nat} (v:t A (S n)) : t A n :=
+Eval cbv delta beta in (rectS (fun n _ => t A n) (fun a => [])
+  (fun h _ _ H => h :: H) _ v).
+
+(** Add an element at the end of a vector *)
+Fixpoint shiftin {A} {n:nat} (a : A) (v:t A n) : t A (S n) :=
+match v with
+  |[] => a :: []
+  |h :: t => h :: (shiftin a t)
+end.
+
+(** Copy last element of a vector *)
+Definition shiftrepeat {A} {n} (v:t A (S n)) : t A (S (S n)) :=
+Eval cbv delta beta in (rectS (fun n _ => t A (S (S n)))
+  (fun h =>  h :: h :: []) (fun h _ _ H => h :: H) _ v).
+
+(** Remove [p] last elements of a vector *)
+Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n
+  -> t A (n - p).
+Proof.
+  induction p as [| p f]; intros H v.
+  rewrite <- minus_n_O.
+  exact v.
+
+  apply shiftout.
+
+  rewrite minus_Sn_m.
+  apply f.
+  auto with *.
+  exact v.
+  auto with *.
+Defined.
+
+(** Concatenation of two vectors *)
+Fixpoint append {A}{n}{p} (v:t A n) (w:t A p):t A (n+p) :=
+  match v with
+  | [] => w
+  | a :: v' => a :: (append v' w)
+  end.
+
+Infix "++" := append.
+
+(** Two definitions of the tail recursive function that appends two lists but
+reverses the first one *)
+
+(** This one has the exact expected computational behavior *)
+Fixpoint rev_append_tail {A n p} (v : t A n) (w: t A p)
+  : t A (tail_plus n p) :=
+  match v with
+  | [] => w
+  | a :: v' => rev_append_tail v' (a :: w)
+  end.
+
+(** This one has a better type *)
+Definition rev_append {A n p} (v: t A n) (w: t A p)
+  :t A (n + p) :=
+eq_rect _ (fun n => t A n) (rev_append_tail v w) _
+  (eq_sym _ _ _ (plus_tail_plus n p)).
+
+(** rev [a₁ ; a₂ ; .. ; an] is [an ; a{n-1} ; .. ; a₁]
+
+Caution : There is a lot of rewrite garbage in this definition *)
+Definition rev {A n} (v : t A n) : t A n :=
+ eq_rect _ (fun n => t A n) (rev_append v [])
+   _ (eq_sym _ _ _ (plus_n_O _)).
+
+End BASES.
+Local Notation "v [@ p ]" := (nth v p) (at level 1).
+
+Section ITERATORS.
+(** * Here are special non dependent useful instantiation of induction
+schemes *)
+
+(** Uniform application on the arguments of the vector *)
+Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n :=
+  fix map_fix {n} (v : t A n) : t B n := match v with
+  | [] => []
+  | a :: v' => (f a) :: (map_fix _ v')
+  end.
+
+(** map2 g [x1 .. xn] [y1 .. yn] = [(g x1 y1) .. (g xn yn)] *)
+Definition map2 {A B C}{n} (g:A -> B -> C) (v1:t A n) (v2:t B n)
+  : t C n :=
+Eval cbv delta beta in rect2 (fun n _ _ => t C n) (nil C)
+  (fun _ _ _ H a b => (g a b) :: H) _ v1 v2.
+
+(** fold_left f b [x1 .. xn] = f .. (f (f b x1) x2) .. xn *)
+Definition fold_left {A B:Type} (f:B->A->B): forall (b:B) {n} (v:t A n), B :=
+  fix fold_left_fix (b:B) n (v : t A n) : B := match v with
+    | [] => b
+    | a :: w => (fold_left_fix (f b a) _ w)
+  end.
+
+(** fold_right f [x1 .. xn] b = f x1 (f x2 .. (f xn b) .. ) *)
+Definition fold_right {A B : Type} (f : A->B->B) :=
+  fix fold_right_fix {n} (v : t A n) (b:B)
+  {struct v} : B :=
+  match v with
+    | [] => b
+    | a :: w => f a (fold_right_fix _ w b)
+  end.
+
+(** fold_right2 g [x1 .. xn] [y1 .. yn] c = g x1 y1 (g x2 y2 .. (g xn yn c) .. ) *)
+Definition fold_right2 {A B C} (g:A -> B -> C -> C) {n} (v:t A n)
+  (w : t B n) (c:C) : C :=
+Eval cbv delta beta in rect2 (fun _ _ _ => C) c
+  (fun _ _ _ H a b => g a b H) _ v w.
+
+(** fold_left2 f b [x1 .. xn] [y1 .. yn] = g .. (g (g a x1 y1) x2 y2) .. xn yn *)
+Definition fold_left2 {A B C: Type} (f : A -> B -> C -> A) :=
+fix fold_left2_fix (a : A) {n} (v : t B n) : t C n -> A :=
+match v in t _ n0 return t C n0 -> A with
+  |[] => fun w => match w in t _ n1
+    return match n1 with |0 => A |S _ => @ID end with
+    |[] => a
+    |_ :: _ => @id end
+  |cons vh vn vt => fun w => match w in t _ n1
+    return match n1 with |0 => @ID |S n => t B n -> A end with
+    |[] => @id
+    |wh :: wt => fun vt' => fold_left2_fix (f a vh wh) _ vt' wt end vt
+end.
+
+End ITERATORS.
+
+Implicit Arguments rectS.
+Implicit Arguments rect2.
+Implicit Arguments fold_left.
+Implicit Arguments fold_right.
+Implicit Arguments map.
+Implicit Arguments fold_left2.
+
+
+Section SCANNING.
+Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop :=
+ |Forall_nil: Forall P []
+ |Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v).
+Hint Constructors Forall.
+
+Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop :=
+ |Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v)
+ |Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v).
+Hint Constructors Exists.
+
+Inductive In {A} (a:A): forall {n}, t A n -> Prop :=
+ |In_cons_hd {m} (v: t A m): In a (a::v)
+ |In_cons_tl {m} x (v: t A m): In a v -> In a (x::v).
+Hint Constructors In.
+
+Inductive Forall2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop :=
+ |Forall2_nil: Forall2 P [] []
+ |Forall2_cons {m} x1 x2 (v1:t A m) v2: P x1 x2 -> Forall2 P v1 v2 ->
+    Forall2 P (x1::v1) (x2::v2).
+Hint Constructors Forall2.
+
+Inductive Exists2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop :=
+ |Exists2_cons_hd {m} x1 x2 (v1: t A m) (v2: t B m): P x1 x2 -> Exists2 P (x1::v1) (x2::v2)
+ |Exists2_cons_tl {m} x1 x2 (v1:t A m) v2: Exists2 P v1 v2 -> Exists2 P (x1::v1) (x2::v2).
+Hint Constructors Exists2.
+
+End SCANNING.
+
+Section VECTORLIST.
+(** * vector <=> list functions *)
+
+Fixpoint of_list {A} (l : list A) : t A (length l) :=
+match l as l' return t A (length l') with
+  |Datatypes.nil => []
+  |(h :: tail)%list => (h :: (of_list tail))
+end.
+
+Definition to_list {A}{n} (v : t A n) : list A :=
+Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.nil.
+End VECTORLIST.
+
+Module VectorNotations.
+Notation "[]" := [] : vector_scope.
+Notation "h :: t" := (h :: t) (at level 60, right associativity)
+  : vector_scope.
+
+Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
+
+Open Scope vector_scope.
+End VectorNotations.
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
new file mode 100644
index 000000000..1fa70a60c
--- /dev/null
+++ b/theories/Vectors/VectorSpec.v
@@ -0,0 +1,113 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Proofs of specification for functions defined over Vector
+
+   Author: Pierre Boutillier
+   Institution: PPS, INRIA 12/2010
+*)
+
+Require Fin.
+Require Import VectorDef.
+Import VectorNotations.
+
+(** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all
+is true for the one that use [lt] *)
+
+Lemma eq_nth_iff A n (v1 v2: t A n):
+  (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2.
+Proof.
+split.
+  revert n v1 v2; refine (rect2 _ _ _); simpl; intros.
+    reflexivity.
+    f_equal. apply (H0 Fin.F1 Fin.F1 eq_refl).
+    apply H. intros p1 p2 H1;
+    apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)).
+  intros; now f_equal.
+Qed.
+
+Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n),
+ nth_order v H = last v.
+Proof.
+unfold nth_order; refine (rectS _ _ _); now simpl.
+Qed.
+
+Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2):
+  nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2.
+Proof.
+subst k2; induction k1.
+  generalize dependent n. apply caseS ; intros. now simpl.
+  generalize dependent n. refine (caseS _ _) ; intros. now simpl.
+Qed.
+
+Lemma shiftin_last A a n (v: t A n): last (shiftin a v) = a.
+Proof.
+induction v ;now simpl.
+Qed.
+
+Lemma shiftrepeat_nth A: forall n k (v: t A (S n)),
+  nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k.
+Proof.
+refine (Fin.rectS _ _ _); intros.
+  revert n v; refine (caseS _ _); simpl; intros. now destruct t.
+  revert p H.
+  refine (match v as v' in t _ m return match m as m' return t A m' -> Type with
+    |S (S n) => fun v => forall p : Fin.t (S n),
+      (forall v0 : t A (S n), (shiftrepeat v0) [@ Fin.L_R 1 p ] = v0 [@p]) ->
+      (shiftrepeat v) [@Fin.L_R 1 (Fin.FS p)] = v [@Fin.FS p]
+    |_ => fun _ => @ID end v' with
+  |[] => @id |h :: t => _ end). destruct n0. exact @id. now simpl.
+Qed.
+
+Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v.
+Proof.
+refine (rectS _ _ _); now simpl.
+Qed.
+
+Lemma const_nth A (a: A) n (p: Fin.t n): (const a n)[@ p] = a.
+Proof.
+now induction p.
+Qed.
+
+Lemma nth_map {A B} (f: A -> B) {n} v (p1 p2: Fin.t n) (eq: p1 = p2):
+  (map f v) [@ p1] = f (v [@ p2]).
+Proof.
+subst p2; induction p1.
+  revert n v; refine (caseS _ _); now simpl.
+  revert n v p1 IHp1; refine (caseS _ _); now simpl.
+Qed.
+
+Lemma nth_map2 {A B C} (f: A -> B -> C) {n} v w (p1 p2 p3: Fin.t n):
+  p1 = p2 -> p2 = p3 -> (map2 f v w) [@p1] = f (v[@p2]) (w[@p3]).
+Proof.
+intros; subst p2; subst p3; revert n v w p1.
+refine (rect2 _ _ _); simpl.
+  exact (Fin.case0).
+  intros n v1 v2 H a b p; revert n p v1 v2 H; refine (Fin.caseS _ _ _);
+    now simpl.
+Qed.
+
+Lemma fold_left_right_assoc_eq {A B} {f: A -> B -> A}
+  (assoc: forall a b c, f (f a b) c = f (f a c) b)
+  {n} (v: t B n): forall a, fold_left f a v = fold_right (fun x y => f y x) v a.
+Proof.
+assert (forall n h (v: t B n) a, fold_left f (f a h) v = f (fold_left f a v) h).
+  induction v0.
+    now simpl.
+    intros; simpl. rewrite<- IHv0. now f_equal.
+  induction v.
+    reflexivity.
+    simpl. intros; now rewrite<- (IHv).
+Qed.
+
+Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l.
+Proof.
+induction l.
+  reflexivity.
+  unfold to_list; simpl. now f_equal.
+Qed.
diff --git a/theories/Vectors/vo.itarget b/theories/Vectors/vo.itarget
new file mode 100644
index 000000000..7f00d0162
--- /dev/null
+++ b/theories/Vectors/vo.itarget
@@ -0,0 +1,4 @@
+Fin.vo
+VectorDef.vo
+VectorSpec.vo
+Vector.vo
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 4e9c85278..4f4a6078c 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -230,4 +230,4 @@ Lemma Zeq_bool_if : forall x y, if Zeq_bool x y then x=y else x<>y.
 Proof.
   intros. generalize (Zeq_bool_eq x y)(Zeq_bool_neq x y).
   destruct Zeq_bool; auto.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v
index 6d8a237e5..ff1d96df4 100644
--- a/theories/ZArith/Zdigits.v
+++ b/theories/ZArith/Zdigits.v
@@ -45,17 +45,17 @@ Section VALUE_OF_BOOLEAN_VECTORS.
     exact 0%Z.
 
     inversion H0.
-    exact (bit_value a + 2 * H H2)%Z.
+    exact (bit_value h + 2 * H H2)%Z.
   Defined.
 
   Lemma two_compl_value : forall n:nat, Bvector (S n) -> Z.
   Proof.
     simple induction n; intros.
     inversion H.
-    exact (- bit_value a)%Z.
+    exact (- bit_value h)%Z.
 
     inversion H0.
-    exact (bit_value a + 2 * H H2)%Z.
+    exact (bit_value h + 2 * H H2)%Z.
   Defined.
 
 End VALUE_OF_BOOLEAN_VECTORS.
@@ -134,7 +134,7 @@ Section Z_BRIC_A_BRAC.
 
   Lemma binary_value_Sn :
     forall (n:nat) (b:bool) (bv:Bvector n),
-      binary_value (S n) (Vcons bool b n bv) =
+      binary_value (S n) ( b :: bv) =
       (bit_value b + 2 * binary_value n bv)%Z.
   Proof.
     intros; auto.
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index 61c31f109..63317d9cb 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -19,4 +19,4 @@ Notation Zmin_max_distr_r := Z.min_max_distr (only parsing).
 Notation Zmax_min_modular_r := Z.max_min_modular (only parsing).
 Notation Zmin_max_modular_r := Z.min_max_modular (only parsing).
 Notation max_min_disassoc := Z.max_min_disassoc (only parsing).
-(*end hide*)
\ No newline at end of file
+(*end hide*)
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 8f4a69b1e..454f62aa9 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -194,7 +194,7 @@ Proof.
 Qed.
 
 (** For compatibility *)
-Definition Zpos_eq_Z_of_nat_o_nat_of_P p := eq_sym (Z_of_nat_of_P p).
+Definition Zpos_eq_Z_of_nat_o_nat_of_P p := eq_sym _ _ _ (Z_of_nat_of_P p).
 
 (******************************************************************)
 (** Properties of the injection from N into Z *)
diff --git a/theories/theories.itarget b/theories/theories.itarget
index 7cc4e09a9..3a87d8cf1 100644
--- a/theories/theories.itarget
+++ b/theories/theories.itarget
@@ -6,6 +6,7 @@ MSets/vo.otarget
 Structures/vo.otarget
 Init/vo.otarget
 Lists/vo.otarget
+Vectors/vo.otarget
 Logic/vo.otarget
 PArith/vo.otarget
 NArith/vo.otarget