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

2 files changed, 3 insertions, 3 deletions

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.