From 303b167ff91e014768ee0286bf8dc0e202778b56 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 15 Dec 2020 20:46:40 -0800
Subject: Modify Bool/DecBool.v to compile with -mangle-names

---
 theories/Bool/DecBool.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index ef78121d63..5eb2a99739 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -18,7 +18,7 @@ Theorem ifdec_left :
   forall (A B:Prop) (C:Set) (H:{A} + {B}),
     ~ B -> forall x y:C, ifdec H x y = x.
 Proof.
-  intros; case H; auto.
+  intros A B C H **; case H; auto.
   intro; absurd B; trivial.
 Qed.
 
@@ -26,7 +26,7 @@ Theorem ifdec_right :
   forall (A B:Prop) (C:Set) (H:{A} + {B}),
     ~ A -> forall x y:C, ifdec H x y = y.
 Proof.
-  intros; case H; auto.
+  intros A B C H **; case H; auto.
   intro; absurd A; trivial.
 Qed.
 
-- 
cgit v1.2.3