1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index b95b25fd..31ff029c 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -6,11 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: DecBool.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: DecBool.v 8866 2006-05-28 16:21:04Z herbelin $ i*)
 
 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.