diff options
| author | Jasper Hugunin | 2020-10-09 16:04:25 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-11 19:05:14 -0700 |
| commit | c3fd4e4e46b0681b2fd2bc1ade5dc489869a507a (patch) | |
| tree | 4cfb037e12a5d5e7b1931528bee64f173d0cb8fc | |
| parent | aab1a1280caca5a2e6b10f230c504771028aee2b (diff) | |
Modify Vectors/VectorDef.v to compile with -mangle-names
| -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. |