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

diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index 5cb4b79d5..ac3233704 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -36,7 +36,7 @@ Proof.
  Apply Acc_intro;Intros.
  Inversion_clear H3;Auto with sets.
  Apply acc_A_sum;Auto with sets.
-Save.
+Qed.
 
 
 Lemma wf_disjoint_sum:
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index db9cfe227..d2658e717 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -20,7 +20,7 @@ Section WfInclusion.
   Proof.
     Induction 2;Intros.
     Apply Acc_intro;Auto with sets.
-  Save.
+  Qed.
 
   Hints Resolve Acc_incl.
 
@@ -28,6 +28,6 @@ Section WfInclusion.
          (inclusion A R1 R2)->(well_founded A R2)->(well_founded A R1).
   Proof.
     Unfold well_founded ;Auto with sets.
-  Save.
+  Qed.
 
 End WfInclusion.
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index 3e4bca83f..f29151cae 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -23,15 +23,15 @@ Section Inverse_Image.
     Apply Acc_intro; Intros.
     Apply (H1 (f y0)); Try Trivial.
     Rewrite H2; Trivial.
-  Save.
+  Qed.
 
   Lemma Acc_inverse_image : (x:A)(Acc B R (f x)) -> (Acc A Rof x).
     Intros; Apply (Acc_lemma (f x)); Trivial.
-  Save.
+  Qed.
 
   Theorem wf_inverse_image: (well_founded B R)->(well_founded A Rof).
     Red; Intros; Apply Acc_inverse_image; Auto.
-  Save.
+  Qed.
 
 End Inverse_Image.
 
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index c57a75133..3e8ba318a 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -74,7 +74,7 @@ Proof.
  Apply acc_A_B_lexprod;Auto with sets;Intros.
  Red in wfB.
  Auto with sets.
-Save.
+Qed.
 
 
 End WfLexicographic_Product.
@@ -104,7 +104,7 @@ Proof.
  (Apply left_lex;Auto with sets).
 
  (Apply right_lex;Auto with sets).
-Save.
+Qed.
 i*)
 
   Lemma Acc_symprod: (x:A)(Acc A leA x)->(y:B)(Acc B leB y)
@@ -116,7 +116,7 @@ Proof.
  Inversion_clear H5;Auto with sets.
  Apply H1;Auto with sets.
  Apply Acc_intro;Auto with sets.
-Save.
+Qed.
 
 
 Lemma wf_symprod: (well_founded A leA)->(well_founded B leB)
@@ -125,7 +125,7 @@ Proof.
  Red.
  Induction a;Intros.
  Apply Acc_symprod;Auto with sets.
-Save.
+Qed.
 
 End Wf_Symmetric_Product.
 
@@ -156,7 +156,7 @@ Proof.
 
  Apply sp_noswap.
  Apply left_sym;Auto with sets.
-Save.
+Qed.
 
 
   Lemma Acc_swapprod: (x,y:A)(Acc A R x)->(Acc A R y)
@@ -184,7 +184,7 @@ Proof.
  Apply right_sym;Auto with sets.
 
  Auto with sets.
-Save.
+Qed.
 
 
   Lemma wf_swapprod: (well_founded A R)->(well_founded A*A SwapProd).
@@ -192,6 +192,6 @@ Proof.
  Red.
  Induction a;Intros.
  Apply Acc_swapprod;Auto with sets.
-Save.
+Qed.
 
 End Swap.
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index 576c83cb4..9c013bd11 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -34,7 +34,7 @@ Proof.
  Elim H4 with x1 ;Auto with sets;Intros.
  Exists x2;Auto with sets.
  Apply t_trans with x1 ;Auto with sets.
-Save.
+Qed.
 
 
   Lemma Acc_union:  (commut A R1 R2)->((x:A)(Acc A R2 x)->(Acc A R1 x))
@@ -61,7 +61,7 @@ Proof.
  Apply Acc_inv with x ;Auto with sets.
  Apply H0.
  Apply Acc_intro;Auto with sets.
-Save.
+Qed.
 
 
   Theorem wf_union:  (commut A R1 R2)->(well_founded A R1)->(well_founded A R2)
@@ -70,6 +70,6 @@ Proof.
  Unfold well_founded .
  Intros.
  Apply Acc_union;Auto with sets.
-Save.
+Qed.
 
 End WfUnion.