From 4c4fb148fa874da2065501d70f757c27685957cd Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 15 Dec 2020 20:45:50 -0800
Subject: Modify Bool/BoolEq.v to compile with -mangle-names

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

diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
index f002ee427c..dd10c758a5 100644
--- a/theories/Bool/BoolEq.v
+++ b/theories/Bool/BoolEq.v
@@ -46,7 +46,7 @@ Section Bool_eq_dec.
 
   Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}.
   Proof.
-    intros.
+    intros x y.
     exists (beq x y).
     constructor.
   Defined.
-- 
cgit v1.2.3