diff options
| author | Théo Zimmermann | 2019-06-20 11:43:01 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-20 11:43:01 +0200 |
| commit | b883efe3bbb16b5f10f3ecd65b2399233dc00e08 (patch) | |
| tree | 9b8d18dad8ba4b99eb55f94f0d181cea07b8d436 | |
| parent | d501690a7d767d4a542867c5b6a65a722fa8c4c1 (diff) | |
Fix coqdoc title: should be on a single line.
Otherwise coqdoc doesn't understand it is still the title.
| -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 := |