From 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Nov 2003 17:28:49 +0000
Subject: Remplacement des fichiers .v ancienne syntaxe de theories, contrib et
 states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Bool/DecBool.v | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

(limited to 'theories/Bool/DecBool.v')

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
-- 
cgit v1.2.3