diff options
| author | Vincent Laporte | 2019-06-25 07:59:22 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-06-25 07:59:22 +0000 |
| commit | 8fa180ecbd34973f866372bee7bd9020626afedb (patch) | |
| tree | 324bde5c49ad25773d51f7a984f8a1022f314b38 | |
| parent | 4fe8612fbfd1581b23bb4c813c900ab687797814 (diff) | |
| parent | b883efe3bbb16b5f10f3ecd65b2399233dc00e08 (diff) | |
Merge PR #10408: Fix coqdoc title: should be on a single line.
Reviewed-by: vbgl
| -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 := |