Uniformisation (Qed/Save et Implicits Arguments)

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

2 files changed, 8 insertions, 8 deletions

diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 5c3a46529..d7cb7a7eb 100755
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -31,7 +31,7 @@ Apply Build_preorder.
 Exact (rt_refl A R).
 
 Exact (rt_trans A R).
-Save.
+Qed.
 
 
 
@@ -42,7 +42,7 @@ Red.
 Induction 1; Auto with sets.
 Intros.
 Apply rt_trans with y0; Auto with sets.
-Save.
+Qed.
 
   Lemma  clos_refl_trans_ind_left: (A:Set)(R:A->A->Prop)(M:A)(P:A->Prop)
            (P M)
@@ -61,7 +61,7 @@ Apply H0; Auto with sets.
 Intros.
 Apply H5 with P0; Auto with sets.
 Apply rt_trans with y; Auto with sets.
-Save.
+Qed.
 
 
 End Clos_Refl_Trans.
@@ -75,7 +75,7 @@ Red.
 Induction 1; Auto with sets.
 Intros.
 Apply rst_trans with y0; Auto with sets.
-Save.
+Qed.
 
   Lemma clos_rst_is_equiv: (equivalence A (clos_refl_sym_trans A R)).
 Apply Build_equivalence.
@@ -84,7 +84,7 @@ Exact (rst_refl A R).
 Exact (rst_trans A R).
 
 Exact (rst_sym A R).
-Save.
+Qed.
 
   Lemma clos_rst_idempotent:
        (incl (clos_refl_sym_trans A (clos_refl_sym_trans A R))
@@ -93,7 +93,7 @@ Red.
 Induction 1; Auto with sets.
 Intros.
 Apply rst_trans with y0; Auto with sets.
-Save.
+Qed.
 
 End Clos_Refl_Sym_Trans.
 
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 60cb9b4d7..86627c8b3 100755
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -16,7 +16,7 @@ Lemma inverse_image_of_equivalence : (A,B:Set)(f:A->B)
   (r:(relation B))(equivalence B r)->(equivalence A [x,y:A](r (f x) (f y))).
 Intros; Split; Elim H; Red; Auto.
 Intros; Apply equiv_trans with (f y); Assumption.
-Save.
+Qed.
 
 Lemma inverse_image_of_eq : (A,B:Set)(f:A->B)
   (equivalence A [x,y:A](f x)=(f y)).
@@ -25,4 +25,4 @@ Split; Red;
 | (* transitivity *) Intros; Transitivity (f y); Assumption
 | (* symmetry *) Intros; Symmetry; Assumption
 ].
-Save.
+Qed.