Field ne fait maintenant que les reductions necessaires

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

3 files changed, 6 insertions, 6 deletions

diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index 005bdb3a1..dcf4e6406 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -750,7 +750,7 @@ Field.
 DiscrR.
 Case delta; Intros.
 Apply prod_neq_R0.
-Red; Intro H13; Rewrite H13 in cond_pos; Elim (Rlt_antirefl ``0`` cond_pos).
+Compute; Intro H13; Rewrite H13 in cond_pos; Elim (Rlt_antirefl ``0`` cond_pos).
 Apply Rinv_neq_R0; DiscrR.
 Replace ``((f (x+delta/2))-(f x))/(delta/2)`` with ``-(((f x)-(f (x+delta/2)))/(delta/2))``.
 Rewrite <- Ropp_O.
@@ -765,7 +765,7 @@ Left; Apply Rlt_Rinv; Assumption.
 Field.
 Case delta; Intros.
 Apply prod_neq_R0.
-Red; Intro H13; Rewrite H13 in cond_pos; Elim (Rlt_antirefl ``0`` cond_pos).
+Compute; Intro H13; Rewrite H13 in cond_pos; Elim (Rlt_antirefl ``0`` cond_pos).
 Apply Rinv_neq_R0; DiscrR.
 Split.
 Unfold Rdiv; Apply prod_neq_R0.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 0c1ad9305..f31429d4a 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -618,8 +618,8 @@ Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H17; Generalize (lt_INR_0 (2) (neq_O_lt (2)
 Replace ``(Rabsolu (f x))*(Rabsolu l)*/2*/(Rabsolu (f x))`` with ``(Rabsolu l)/2``.
 Replace ``(Rabsolu (f x))*(Rabsolu l)*/2*(2*/(Rabsolu l))`` with ``(Rabsolu (f x))``.
 Assumption.
-Field; Apply prod_neq_R0; [DiscrR | Case (case_Rabsolu l); Intro; [Apply Ropp_neq; Assumption | Assumption]].
-Unfold Rdiv; Field; Apply prod_neq_R0; [DiscrR | Case (case_Rabsolu (f x)); Intro; [Apply Ropp_neq; Assumption | Assumption]].
+Field; Apply prod_neq_R0; [DiscrR | Unfold Rabsolu; Case (case_Rabsolu l); Intro; [Apply Ropp_neq; Assumption | Assumption]].
+Unfold Rdiv; Field; Apply prod_neq_R0; [DiscrR | Unfold Rabsolu; Case (case_Rabsolu (f x)); Intro; [Apply Ropp_neq; Assumption | Assumption]].
 Apply Rabsolu_no_R0; Assumption.
 Apply Rabsolu_no_R0; Assumption.
 Apply Rabsolu_no_R0; Assumption.
@@ -631,7 +631,7 @@ Intro; Elim (Rlt_antirefl ``0`` (Rlt_trans ``0`` ``(Rabsolu l)/2`` ``0`` H17 H15
 Unfold Rdiv; Apply Rmult_lt_pos.
 Apply Rabsolu_pos_lt; Assumption.
 Apply Rlt_Rinv; Cut ~(O=(2)); [Intro H17; Generalize (lt_INR_0 (2) (neq_O_lt (2) H17)); Unfold INR; Intro; Assumption | Discriminate].
-Unfold Rdiv; Field; DiscrR.
+Field; DiscrR.
 Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Apply Rmin_r]].
 Split; [Assumption | Apply Rlt_le_trans with (Rmin delta1 delta2); [Assumption | Apply Rmin_l]].
 Change ``0<eps*(Rsqr l)/2``; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Repeat Apply Rmult_lt_pos.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 1115ec19f..d1fc539f8 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -264,7 +264,7 @@ Intros; Elim (sin_eq_0 x); Intros; Apply  (H1 H).
 Save.
 
 Lemma cos_eq_0_0 : (x:R) (cos x)==R0 -> (EXT k : Z | ``x==(IZR k)*PI+PI/2``). 
-Intros x H; Rewrite -> cos_sin in H; Generalize (sin_eq_0_0 (Rplus (Rdiv PI (INR (2))) x) H); Intro H2; Elim H2; Intros x0 H3; Exists (Zminus x0 (inject_nat (S O))); Rewrite <- Z_R_minus; Ring; Rewrite Rmult_sym; Rewrite <- H3; Field; DiscrR.
+Intros x H; Rewrite -> cos_sin in H; Generalize (sin_eq_0_0 (Rplus (Rdiv PI (INR (2))) x) H); Intro H2; Elim H2; Intros x0 H3; Exists (Zminus x0 (inject_nat (S O))); Rewrite <- Z_R_minus; Ring; Rewrite Rmult_sym; Rewrite <- H3; Unfold INR; Field; DiscrR.
 Save.
 
 Lemma  cos_eq_0_1 : (x:R) (EXT k : Z | ``x==(IZR k)*PI+PI/2``) -> ``(cos x)==0``.