From 6e0585f4b05c92f3dfebdd0bc6907e1b0cce1f4a Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Fri, 9 Oct 2020 15:36:18 -0700
Subject: Modify Bool/Sumbool.v to compile with -mangle-names

---
 theories/Bool/Sumbool.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index bea14480f8..52605a4667 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -16,7 +16,7 @@
 (** A boolean is either [true] or [false], and this is decidable *)
 
 Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}.
-  destruct b; auto.
+  intros b; destruct b; auto.
 Defined.
 
 Hint Resolve sumbool_of_bool: bool.
@@ -24,13 +24,13 @@ Hint Resolve sumbool_of_bool: bool.
 Definition bool_eq_rec :
   forall (b:bool) (P:bool -> Set),
     (b = true -> P true) -> (b = false -> P false) -> P b.
-  destruct b; auto.
+  intros b; destruct b; auto.
 Defined.
 
 Definition bool_eq_ind :
   forall (b:bool) (P:bool -> Prop),
     (b = true -> P true) -> (b = false -> P false) -> P b.
-  destruct b; auto.
+  intros b; destruct b; auto.
 Defined.
 
 
-- 
cgit v1.2.3