From c3fd4e4e46b0681b2fd2bc1ade5dc489869a507a Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 16:04:25 -0700
Subject: Modify Vectors/VectorDef.v to compile with -mangle-names

---
 theories/Vectors/VectorDef.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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.
 
-- 
cgit v1.2.3