Uniformisation (Qed/Save et Implicits Arguments)

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

3 files changed, 27 insertions, 27 deletions

diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 84649e7a85..82464b3af7 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -13,46 +13,46 @@ Definition decidable := [P:Prop] P \/ ~P.
 
 Theorem dec_not_not : (P:Prop)(decidable P) -> (~P -> False) -> P.
 Unfold decidable; Tauto. 
-Save.
+Qed.
 
 Theorem dec_True: (decidable True).
 Unfold decidable; Auto.
-Save.
+Qed.
 
 Theorem dec_False: (decidable False).
 Unfold decidable not; Auto.
-Save.
+Qed.
 
 Theorem dec_or: (A,B:Prop)(decidable A) -> (decidable B) -> (decidable (A\/B)).
 Unfold decidable; Tauto. 
-Save.
+Qed.
 
 Theorem dec_and: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A/\B)).
 Unfold decidable; Tauto. 
-Save.
+Qed.
 
 Theorem dec_not: (A:Prop)(decidable A) -> (decidable ~A).
 Unfold decidable; Tauto. 
-Save.
+Qed.
 
 Theorem dec_imp: (A,B:Prop)(decidable A) -> (decidable B) ->(decidable (A->B)).
 Unfold decidable; Tauto. 
-Save.
+Qed.
 
 Theorem not_not : (P:Prop)(decidable P) -> (~(~P)) -> P.
-Unfold decidable; Tauto. Save.
+Unfold decidable; Tauto. Qed.
 
 Theorem not_or : (A,B:Prop) ~(A\/B) -> ~A /\ ~B.
-Tauto. Save.
+Tauto. Qed.
 
 Theorem not_and : (A,B:Prop) (decidable A) -> ~(A/\B) -> ~A \/ ~B.
-Unfold decidable; Tauto. Save.
+Unfold decidable; Tauto. Qed.
 
 Theorem not_imp : (A,B:Prop) (decidable A) -> ~(A -> B) -> A /\ ~B.
 Unfold decidable;Tauto.
-Save.
+Qed.
 
 Theorem imp_simp : (A,B:Prop) (decidable A) -> (A -> B) -> ~A \/ B.
 Unfold decidable; Tauto.
-Save.
+Qed.
 
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 7daff9ba30..8f7e76d51d 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -34,12 +34,12 @@ Set Implicit Arguments.
   Lemma eq_eqT_bij: (A:Set)(x,y:A)(p:x=y)p==(eqT2eq (eq2eqT p)).
 Intros.
 Case p; Reflexivity.
-Save.
+Qed.
 
   Lemma eqT_eq_bij: (A:Set)(x,y:A)(p:x==y)p==(eq2eqT (eqT2eq p)).
 Intros.
 Case p; Reflexivity.
-Save.
+Qed.
 
 
 Section DecidableEqDep.
@@ -52,7 +52,7 @@ Section DecidableEqDep.
   Remark trans_sym_eqT: (x,y:A)(u:x==y)(comp u u)==(refl_eqT ? y).
 Intros.
 Case u; Trivial.
-Save.
+Qed.
 
 
 
@@ -74,7 +74,7 @@ Case (eq_dec x y); Intros.
 Reflexivity.
 
 Case n; Trivial.
-Save.
+Qed.
 
 
   Local nu_inv [y:A]: x==y->x==y := [v](comp (nu (refl_eqT ? x)) v).
@@ -84,7 +84,7 @@ Save.
 Intros.
 Case u; Unfold nu_inv.
 Apply trans_sym_eqT.
-Save.
+Qed.
 
 
   Theorem eq_proofs_unicity: (y:A)(p1,p2:x==y) p1==p2.
@@ -93,13 +93,13 @@ Elim nu_left_inv with u:=p1.
 Elim nu_left_inv with u:=p2.
 Elim nu_constant with y p1 p2.
 Reflexivity.
-Save.
+Qed.
 
   Theorem K_dec: (P:x==x->Prop)(P (refl_eqT ? x)) -> (p:x==x)(P p).
 Intros.
 Elim eq_proofs_unicity with x (refl_eqT ? x) p.
 Trivial.
-Save.
+Qed.
 
 
   (** The corollary *)
@@ -128,7 +128,7 @@ Case n; Trivial.
 
 Case H.
 Reflexivity.
-Save.
+Qed.
 
 End DecidableEqDep.
 
@@ -146,4 +146,4 @@ Elim e; Left ; Reflexivity.
 Right ; Red; Intro neq; Apply n; Elim neq; Reflexivity.
 
 Trivial.
-Save.
+Qed.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 42f9585477..a44edfbf27 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -19,29 +19,29 @@ Hints Resolve JMeq_refl.
 
 Lemma JMeq_sym : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x).
 NewDestruct 1; Trivial.
-Save.
+Qed.
 
 Hints Immediate JMeq_sym.
 
 Lemma JMeq_trans : (A,B,C:Set)(x:A)(y:B)(z:C)
 	(JMeq x y)->(JMeq y z)->(JMeq x z).
 NewDestruct 1; Trivial.
-Save.
+Qed.
 
 Axiom JMeq_eq : (A:Set)(x,y:A)(JMeq x y)->(x=y).
 
 Lemma JMeq_eq_ind : (A:Set)(x,y:A)(P:A->Prop)(P x)->(JMeq x y)->(P y).
 Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial.
-Save.
+Qed.
 
 Lemma JMeq_eq_rec : (A:Set)(x,y:A)(P:A->Set)(P x)->(JMeq x y)->(P y).
 Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial.
-Save.
+Qed.
 
 Lemma JMeq_eq_ind_r : (A:Set)(x,y:A)(P:A->Prop)(P y)->(JMeq x y)->(P x).
 Intros A x y P H H'; Case JMeq_eq with 1:=(JMeq_sym H'); Trivial.
-Save.
+Qed.
 
 Lemma JMeq_eq_rec_r : (A:Set)(x,y:A)(P:A->Set)(P y)->(JMeq x y)->(P x).
 Intros A x y P H H'; Case JMeq_eq with 1:=(JMeq_sym H'); Trivial.
-Save.
+Qed.