aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Vectors
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Vectors')
-rw-r--r--theories/Vectors/VectorDef.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index c49451776..a21b9ca98 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -305,12 +305,10 @@ End VECTORLIST.
Module VectorNotations.
Delimit Scope vector_scope with vector.
Notation "[ ]" := [] (format "[ ]") : vector_scope.
-Notation "[]" := [] (compat "8.5") : vector_scope.
Notation "h :: t" := (h :: t) (at level 60, right associativity)
: vector_scope.
Notation "[ x ]" := (x :: []) : vector_scope.
Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope.
-Notation "[ x ; .. ; y ]" := (cons _ x _ .. (cons _ y _ (nil _)) ..) (compat "8.4") : vector_scope.
Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
Open Scope vector_scope.
End VectorNotations.