Uniformisation (Qed/Save et Implicits Arguments)

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

5 files changed, 69 insertions, 69 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 1942ca6b3..cfd6f656a 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -23,12 +23,12 @@ Hints Unfold Is_true : bool.
 Lemma Is_true_eq_left : (x:bool)x=true -> (Is_true x).
 Proof.
   Intros; Rewrite H; Auto with bool.
-Save.
+Qed.
 
 Lemma Is_true_eq_right : (x:bool)true=x -> (Is_true x).
 Proof.
   Intros; Rewrite <- H; Auto with bool.
-Save.
+Qed.
 
 Hints Immediate Is_true_eq_right Is_true_eq_left : bool.
 
@@ -40,7 +40,7 @@ Lemma diff_true_false : ~true=false.
 Goal.
 Unfold not; Intro contr; Change (Is_true false).
 Elim contr; Simpl; Trivial with bool.
-Save.
+Qed.
 Hints Resolve diff_true_false : bool v62.
 
 Lemma diff_false_true : ~false=true.
@@ -48,12 +48,12 @@ Goal.
 Red; Intros H; Apply diff_true_false.
 Symmetry.
 Assumption.
-Save.
+Qed.
 Hints Resolve diff_false_true : bool v62.
 
 Lemma eq_true_false_abs : (b:bool)(b=true)->(b=false)->False.
 Intros b H; Rewrite H; Auto with bool.
-Save.
+Qed.
 Hints Resolve eq_true_false_abs : bool.
 
 Lemma not_true_is_false : (b:bool)~b=true->b=false.
@@ -63,7 +63,7 @@ Red in H; Elim H.
 Reflexivity.
 Intros abs.
 Reflexivity.
-Save.
+Qed.
 
 Lemma not_false_is_true : (b:bool)~b=false->b=true.
 NewDestruct b.
@@ -71,7 +71,7 @@ Intros.
 Reflexivity.
 Intro H; Red in H; Elim H.
 Reflexivity.
-Save.
+Qed.
 
 (**********************)
 (** Order on booleans *)
@@ -99,19 +99,19 @@ Definition eqb : bool->bool->bool :=
 
 Lemma eqb_refl : (x:bool)(Is_true (eqb x x)).
 NewDestruct x; Simpl; Auto with bool.
-Save.
+Qed.
 
 Lemma eqb_eq : (x,y:bool)(Is_true (eqb x y))->x=y.
 NewDestruct x; NewDestruct y; Simpl; Tauto.
-Save.
+Qed.
 
 Lemma Is_true_eq_true : (x:bool) (Is_true x) -> x=true.
 NewDestruct x; Simpl; Tauto.
-Save.
+Qed.
  
 Lemma Is_true_eq_true2 : (x:bool)  x=true -> (Is_true x).
 NewDestruct x; Simpl; Auto with bool.
-Save.
+Qed.
 
 Lemma eqb_subst : 
   (P:bool->Prop)(b1,b2:bool)(eqb b1 b2)=true->(P b1)->(P b2).
@@ -127,19 +127,19 @@ Case b2.
 Intros H.
 Inversion_clear H.
 Trivial with bool.
-Save.
+Qed.
 
 Lemma eqb_reflx : (b:bool)(eqb b b)=true.
 Intro b.
 Case b.
 Trivial with bool.
 Trivial with bool.
-Save.
+Qed.
 
 Lemma eqb_prop : (a,b:bool)(eqb a b)=true -> a=b.
 NewDestruct a; NewDestruct b; Simpl; Intro;
   Discriminate H Orelse Reflexivity.
-Save.
+Qed.
 
 
 (************************)
@@ -180,12 +180,12 @@ Definition negb := [b:bool]Cases b of
 Lemma negb_intro : (b:bool)b=(negb (negb b)).
 Goal.
 Induction b; Reflexivity.
-Save.
+Qed.
 
 Lemma negb_elim : (b:bool)(negb (negb b))=b.
 Goal.
 Induction b; Reflexivity.
-Save.
+Qed.
        
 Lemma negb_orb : (b1,b2:bool)
   (negb (orb b1 b2)) = (andb (negb b1) (negb b2)).
@@ -202,24 +202,24 @@ Qed.
 Lemma negb_sym : (b,b':bool)(b'=(negb b))->(b=(negb b')).
 Goal.
 Induction b; Induction b'; Intros; Simpl; Trivial with bool.
-Save.
+Qed.
 
 Lemma no_fixpoint_negb : (b:bool)~(negb b)=b.
 Goal.
 Induction b; Simpl; Unfold not; Intro; Apply diff_true_false; Auto with bool.
-Save.
+Qed.
 
 Lemma eqb_negb1 : (b:bool)(eqb (negb b) b)=false.
 NewDestruct b.
 Trivial with bool.
 Trivial with bool.
-Save.
+Qed.
  
 Lemma eqb_negb2 : (b:bool)(eqb b (negb b))=false.
 NewDestruct b.
 Trivial with bool.
 Trivial with bool.
-Save.
+Qed.
 
 
 Lemma if_negb : (A:Set) (b:bool) (x,y:A) (if (negb b) then x else y)=(if b then y else x).
@@ -235,12 +235,12 @@ Qed.
 Lemma orb_prop : 
   (a,b:bool)(orb a b)=true -> (a = true)\/(b = true).
 Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool.
-Save.
+Qed.
 
 Lemma orb_prop2 : 
   (a,b:bool)(Is_true (orb a b)) -> (Is_true a)\/(Is_true b).
 Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool.
-Save.
+Qed.
 
 Lemma orb_true_intro 
     : (b1,b2:bool)(b1=true)\/(b2=true)->(orb b1 b2)=true.
@@ -248,37 +248,37 @@ NewDestruct b1; Auto with bool.
 NewDestruct 1; Intros.
 Elim diff_true_false; Auto with bool.
 Rewrite H; Trivial with bool.
-Save.
+Qed.
 Hints Resolve orb_true_intro : bool v62.
 
 Lemma orb_b_true : (b:bool)(orb b true)=true.
 Auto with bool.
-Save.
+Qed.
 Hints Resolve orb_b_true : bool v62.
 
 Lemma orb_true_b : (b:bool)(orb true b)=true.
 Trivial with bool.
-Save.
+Qed.
 
 Lemma orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}.
 NewDestruct b1; Simpl; Auto with bool.
-Save.
+Qed.
 Lemma orb_false_intro 
     : (b1,b2:bool)(b1=false)->(b2=false)->(orb b1 b2)=false.
 Intros b1 b2 H1 H2; Rewrite H1; Rewrite H2; Trivial with bool.
-Save.
+Qed.
 Hints Resolve orb_false_intro : bool v62.
 
 Lemma orb_b_false : (b:bool)(orb b false)=b.
 Proof.
   NewDestruct b; Trivial with bool.
-Save.
+Qed.
 Hints Resolve orb_b_false : bool v62.
 
 Lemma orb_false_b : (b:bool)(orb false b)=b.
 Proof.
   NewDestruct b; Trivial with bool.
-Save.
+Qed.
 Hints Resolve orb_false_b : bool v62.
 
 Lemma orb_false_elim : 
@@ -289,23 +289,23 @@ Proof.
   NewDestruct b2.
   Intros; Elim diff_true_false; Auto with bool.
   Auto with bool.
-Save.
+Qed.
 
 Lemma orb_neg_b :
   (b:bool)(orb b (negb b))=true.
 Proof.
   NewDestruct b; Reflexivity.
-Save.
+Qed.
 Hints Resolve orb_neg_b : bool v62.
 
 Lemma orb_sym : (b1,b2:bool)(orb b1 b2)=(orb b2 b1).
 NewDestruct b1; NewDestruct b2; Reflexivity.
-Save.
+Qed.
 
 Lemma orb_assoc : (b1,b2,b3:bool)(orb b1 (orb b2 b3))=(orb (orb b1 b2) b3).
 Proof.
   NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
-Save.
+Qed.
 
 Hints Resolve orb_sym orb_assoc orb_b_false orb_false_b : bool v62.
 
@@ -319,7 +319,7 @@ Lemma andb_prop :
 Proof.
   Induction a; Induction b; Simpl; Try (Intro H;Discriminate H);
   Auto with bool.
-Save.
+Qed.
 Hints Resolve andb_prop : bool v62.
 
 Definition andb_true_eq : (a,b:bool) true = (andb a b) -> true = a /\ true = b.
@@ -332,67 +332,67 @@ Lemma andb_prop2 :
 Proof.
   Induction a; Induction b; Simpl; Try (Intro H;Discriminate H);
   Auto with bool.
-Save.
+Qed.
 Hints Resolve andb_prop2 : bool v62.
 
 Lemma andb_true_intro : (b1,b2:bool)(b1=true)/\(b2=true)->(andb b1 b2)=true.
 Proof.
   NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
-Save.
+Qed.
 Hints Resolve andb_true_intro : bool v62.
 
 Lemma andb_true_intro2 : 
   (b1,b2:bool)(Is_true b1)->(Is_true b2)->(Is_true (andb b1 b2)).
 Proof.
   NewDestruct b1; NewDestruct b2; Simpl; Tauto.
-Save.
+Qed.
 Hints Resolve andb_true_intro2 : bool v62.
 
 Lemma andb_false_intro1 
     : (b1,b2:bool)(b1=false)->(andb b1 b2)=false.
 NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
-Save.
+Qed.
 
 Lemma andb_false_intro2 
     : (b1,b2:bool)(b2=false)->(andb b1 b2)=false.
 NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool.
-Save.
+Qed.
 
 Lemma andb_b_false : (b:bool)(andb b false)=false.
 NewDestruct b; Auto with bool.
-Save.
+Qed.
 
 Lemma andb_false_b : (b:bool)(andb false b)=false.
 Trivial with bool.
-Save.
+Qed.
 
 Lemma andb_b_true : (b:bool)(andb b true)=b.
 NewDestruct b; Auto with bool.
-Save.
+Qed.
 
 Lemma andb_true_b : (b:bool)(andb true b)=b.
 Trivial with bool.
-Save.
+Qed.
 
 Lemma andb_false_elim : 
     (b1,b2:bool)(andb b1 b2)=false -> {b1=false}+{b2=false}.
 NewDestruct b1; Simpl; Auto with bool.
-Save.
+Qed.
 Hints Resolve andb_false_elim : bool v62.
 
 Lemma andb_neg_b :
    (b:bool)(andb b (negb b))=false.
 NewDestruct b; Reflexivity.
-Save.   
+Qed.   
 Hints Resolve andb_neg_b : bool v62.
 
 Lemma andb_sym : (b1,b2:bool)(andb b1 b2)=(andb b2 b1).
 NewDestruct b1; NewDestruct b2; Reflexivity.
-Save.
+Qed.
 
 Lemma andb_assoc : (b1,b2,b3:bool)(andb b1 (andb b2 b3))=(andb (andb b1 b2) b3).
 NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
-Save.
+Qed.
 
 Hints Resolve andb_sym andb_assoc : bool v62.
 
@@ -469,22 +469,22 @@ Qed.
 Lemma demorgan1 : (b1,b2,b3:bool)
   (andb b1 (orb b2 b3)) = (orb (andb b1 b2) (andb b1 b3)).
 NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
-Save.
+Qed.
 
 Lemma demorgan2 : (b1,b2,b3:bool)
   (andb (orb b1 b2) b3) = (orb (andb b1 b3) (andb b2 b3)).
 NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
-Save.
+Qed.
 
 Lemma demorgan3 : (b1,b2,b3:bool)
   (orb b1 (andb b2 b3)) = (andb (orb b1 b2) (orb b1 b3)).
 NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
-Save.
+Qed.
 
 Lemma demorgan4 : (b1,b2,b3:bool)
   (orb (andb b1 b2) b3) = (andb (orb b1 b3) (orb b2 b3)).
 NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity.
-Save.
+Qed.
 
 Lemma absoption_andb : (b1,b2:bool)
   (andb b1 (orb b1 b2)) = b1.
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.
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index d0c089c7a..48180678f 100755
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -19,31 +19,31 @@ Hints Resolve Iftrue Iffalse : bool v62.
 Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A.
 NewDestruct 1; Intros; Auto with bool.
 Case diff_true_false; Auto with bool.
-Save.
+Qed.
 
 Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B.
 NewDestruct 1; Intros; Auto with bool.
 Case diff_true_false; Trivial with bool.
-Save.
+Qed.
 
 Lemma IfProp_true : (A,B:Prop)(IfProp A B true) -> A.
 Intros.
 Inversion H.
 Assumption.
-Save.
+Qed.
 
 Lemma IfProp_false : (A,B:Prop)(IfProp A B false) -> B.
 Intros.
 Inversion H.
 Assumption.
-Save.
+Qed.
 
 Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B.
 NewDestruct 1; Auto with bool.
-Save.
+Qed.
 
 Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}.
 NewDestruct b; Intro H.
 Left; Inversion H; Auto with bool.
 Right; Inversion H; Auto with bool.
-Save.
+Qed.
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.
 
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index 4422a03f4..07b4c68c8 100755
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -16,18 +16,18 @@ Definition zerob : nat->bool
 
 Lemma zerob_true_intro : (n:nat)(n=O)->(zerob n)=true.
 NewDestruct n; [Trivial with bool | Inversion 1].
-Save.
+Qed.
 Hints Resolve zerob_true_intro : bool.
 
 Lemma zerob_true_elim : (n:nat)(zerob n)=true->(n=O).
 NewDestruct n; [Trivial with bool | Inversion 1].
-Save.
+Qed.
 
 Lemma zerob_false_intro : (n:nat)~(n=O)->(zerob n)=false.
 NewDestruct n; [NewDestruct 1; Auto with bool | Trivial with bool].
-Save.
+Qed.
 Hints Resolve zerob_false_intro : bool.
 
 Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O).
 NewDestruct n; [Intro H; Inversion H | Auto with bool].
-Save.
+Qed.