Modify Bool/DecBool.v to compile with -mangle-names

1 files 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.