diff options
Diffstat (limited to 'theories/Vectors/VectorDef.v')
| -rw-r--r-- | theories/Vectors/VectorDef.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index e5bb66a20..150342ee8 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -34,8 +34,8 @@ Section SCHEMES. (** An induction scheme for non-empty vectors *) Definition rectS {A} (P:forall {n}, t A (S n) -> Type) - (bas: forall a: A, P 0 (a :: [])) - (rect: forall a {n} (v: t A (S n)), P n v -> P (S n) (a :: v)) := + (bas: forall a: A, P (a :: [])) + (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) := fix rectS_fix {n} (v: t A (S n)) : P n v := match v with |nil => @id |