Uniformisation (Qed/Save et Implicits Arguments)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index 8daabd479..28ef57eac 100755
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -17,11 +17,11 @@ Definition ifdec : (A,B:Prop)(C:Set)({A}+{B})->C->C->C
 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.
-Save.
+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.
-Save.
+Qed.
 
 Unset Implicit Arguments.