diff options
| -rw-r--r-- | theories/Vectors/VectorDef.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 3bed8c1e40..20a8581d46 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -217,8 +217,7 @@ End BASES. Local Notation "v [@ p ]" := (nth v p) (at level 1). Section ITERATORS. -(** * Here are special non dependent useful instantiation of induction -schemes *) +(** * 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 := |