From 4d4d2128d2dc761a1b3e002780b865f77fe61e67 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 16:30:39 -0700
Subject: Modify Vectors/VectorEq.v to compile with -mangle-names

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

diff --git a/theories/Vectors/VectorEq.v b/theories/Vectors/VectorEq.v
index 6bd2c30205..c36917aa90 100644
--- a/theories/Vectors/VectorEq.v
+++ b/theories/Vectors/VectorEq.v
@@ -36,7 +36,7 @@ Section BEQ.
   (Hbeq: eqb v1 v2 = true), m = n.
  Proof.
    intros m n v1; revert n.
-   induction v1; destruct v2;
+   induction v1; intros ? v2; destruct v2;
      [now constructor | discriminate | discriminate | simpl].
    intros Hbeq; apply andb_prop in Hbeq; destruct Hbeq.
    f_equal; eauto.
-- 
cgit v1.2.3