1 files changed, 13 insertions, 9 deletions
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index 28ef57eacf..8a15e7624f 100755
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -10,18 +10,22 @@
 
 Set Implicit Arguments.
 
-Definition ifdec : (A,B:Prop)(C:Set)({A}+{B})->C->C->C
-   := [A,B,C,H,x,y]if H then [_]x else [_]y.
+Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C :=
+  if H then fun _ => x else fun _ => y.
 
 
-Theorem ifdec_left : (A,B:Prop)(C:Set)(H:{A}+{B})~B->(x,y:C)(ifdec H x y)=x.
-Intros; Case H; Auto.
-Intro; Absurd B; Trivial.
+Theorem ifdec_left :
+ forall (A B:Prop) (C:Set) (H:{A} + {B}),
+   ~ B -> forall x y:C, ifdec H x y = x.
+intros; case H; auto.
+intro; absurd B; trivial.
 Qed.
 
-Theorem ifdec_right : (A,B:Prop)(C:Set)(H:{A}+{B})~A->(x,y:C)(ifdec H x y)=y.
-Intros; Case H; Auto.
-Intro; Absurd A; Trivial.
+Theorem ifdec_right :
+ forall (A B:Prop) (C:Set) (H:{A} + {B}),
+   ~ A -> forall x y:C, ifdec H x y = y.
+intros; case H; auto.
+intro; absurd A; trivial.
 Qed.
 
-Unset Implicit Arguments.
+Unset Implicit Arguments.
+\ No newline at end of file