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

1 files changed, 13 insertions, 9 deletions

diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index 28ef57eac..8a15e7624 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