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

11 files changed, 11 insertions, 11 deletions

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.