1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index 7fa518d66..82363fff7 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -10,7 +10,7 @@
 
 Set Implicit Arguments.
 
-Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C :=
+Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C :=
   if H then x else y.
 
 
@@ -28,4 +28,4 @@ intros; case H; auto.
 intro; absurd A; trivial.
 Qed.
 
-Unset Implicit Arguments.
-\ No newline at end of file
+Unset Implicit Arguments.