From 7f6883f9a5a6593e667ba4e21fdeccda5c80c589 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Tue, 15 Dec 2020 20:47:27 -0800
Subject: Modify Bool/IfProp.v to compile with -mangle-names

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

diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 7e9087c377..8366e8257e 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -29,13 +29,13 @@ case diff_true_false; trivial with bool.
 Qed.
 
 Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A.
-intros.
+intros A B H.
 inversion H.
 assumption.
 Qed.
 
 Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B.
-intros.
+intros A B H.
 inversion H.
 assumption.
 Qed.
@@ -45,7 +45,7 @@ destruct 1; auto with bool.
 Qed.
 
 Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}.
-destruct b; intro H.
+intros A B b; destruct b; intro H.
 - left; inversion H; auto with bool.
 - right; inversion H; auto with bool.
 Qed.
-- 
cgit v1.2.3