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, 6 insertions, 6 deletions

diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
index 44311a127..817212909 100644
--- a/theories/Bool/Sumbool.v
+++ b/theories/Bool/Sumbool.v
@@ -18,19 +18,19 @@
 Lemma sumbool_of_bool : (b:bool) {b=true}+{b=false}.
 Proof.
   Induction b; Auto.
-Save.
+Qed.
 
 Hints Resolve sumbool_of_bool : bool.
 
 Lemma bool_eq_rec : (b:bool)(P:bool->Set)
                     ((b=true)->(P true))->((b=false)->(P false))->(P b).
 Induction b; Auto.
-Save.
+Qed.
 
 Lemma bool_eq_ind : (b:bool)(P:bool->Prop)
                     ((b=true)->(P true))->((b=false)->(P false))->(P b).
 Induction b; Auto.
-Save.
+Qed.
 
 
 (*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno i*)
@@ -47,17 +47,17 @@ Hypothesis H2 : {C}+{D}.
 Lemma sumbool_and : {A/\C}+{B\/D}.
 Proof.
 Case H1; Case H2; Auto.
-Save.
+Qed.
 
 Lemma sumbool_or : {A\/C}+{B/\D}.
 Proof.
 Case H1; Case H2; Auto.
-Save.
+Qed.
 
 Lemma sumbool_not : {B}+{A}.
 Proof.
 Case H1; Auto.
-Save.
+Qed.
 
 End connectives.