changement de pose en set (pose n'etait pas utilise avec la semantique

 documentee).
Reste a retablir la semantique de pose.


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

1 files changed, 7 insertions, 7 deletions

diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index d29193ad7..f2b2bcd85 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -20,8 +20,8 @@ Definition Majxy (x y:R) (n:nat) : R :=
 
 Lemma Majxy_cv_R0 : forall x y:R, Un_cv (Majxy x y) 0.
 intros.
-pose (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
-pose (C0 := C ^ 4).
+set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
+set (C0 := C ^ 4).
 cut (0 < C).
 intro.
 cut (0 < C0).
@@ -69,7 +69,7 @@ Lemma reste1_maj :
  forall (x y:R) (N:nat),
    (0 < N)%nat -> Rabs (Reste1 x y N) <= Majxy x y (pred N).
 intros.
-pose (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
+set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
 unfold Reste1 in |- *.
 apply Rle_trans with
  (sum_f_R0
@@ -454,7 +454,7 @@ Qed.
 Lemma reste2_maj :
  forall (x y:R) (N:nat), (0 < N)%nat -> Rabs (Reste2 x y N) <= Majxy x y N.
 intros.
-pose (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
+set (C := Rmax 1 (Rmax (Rabs x) (Rabs y))).
 unfold Reste2 in |- *.
 apply Rle_trans with
  (sum_f_R0
@@ -926,8 +926,8 @@ Qed.
 Lemma reste_cv_R0 : forall x y:R, Un_cv (Reste x y) 0.
 intros.
 unfold Reste in |- *.
-pose (An := fun n:nat => Reste2 x y n).
-pose (Bn := fun n:nat => Reste1 x y (S n)).
+set (An := fun n:nat => Reste2 x y n).
+set (Bn := fun n:nat => Reste1 x y (S n)).
 cut
  (Un_cv (fun n:nat => An n - Bn n) (0 - 0) ->
   Un_cv (fun N:nat => Reste2 x y N - Reste1 x y (S N)) 0).
@@ -979,7 +979,7 @@ cut (0 < eps / 3);
 elim (H4 (eps / 3) H7); intros N1 H8. 
 elim (H5 (eps / 3) H7); intros N2 H9. 
 elim (H6 (eps / 3) H7); intros N3 H10.
-pose (N := S (S (max (max N1 N2) N3))). 
+set (N := S (S (max (max N1 N2) N3))). 
 exists N. 
 intros. 
 cut (n = S (pred n)).