diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Vectors/VectorDef.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 57241e5f42..a154a2b269 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -167,7 +167,7 @@ Fixpoint take {A} {n} (p:nat) (le:p <= n) (v:t A n) : t A p := Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n -> t A (n - p). Proof. - induction p as [| p f]; intros H v. + intros A n p; induction p as [| p f]; intros H v. rewrite <- minus_n_O. exact v. |