simplif de la partie ML de ring/field

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

3 files changed, 38 insertions, 34 deletions

diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
new file mode 100644
index 000000000..d285fef30
--- /dev/null
+++ b/theories/Reals/LegacyRfield.v
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Raxioms.
+Require Export LegacyField.
+Import LegacyRing_theory.
+Open Scope R_scope.
+
+Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
+  split.
+  exact Rplus_comm.
+  symmetry  in |- *; apply Rplus_assoc.
+  exact Rmult_comm.
+  symmetry  in |- *; apply Rmult_assoc.
+  intro; apply Rplus_0_l.
+  intro; apply Rmult_1_l.
+  exact Rplus_opp_r.
+  intros.
+  rewrite Rmult_comm.
+  rewrite (Rmult_comm n p).
+  rewrite (Rmult_comm m p).
+  apply Rmult_plus_distr_l.
+  intros; contradiction.
+Defined.
+
+Add Legacy Field
+R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
+  with minus := Rminus div := Rdiv.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 1996eaa97..daebd9178 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -16,42 +16,12 @@ Require Export Raxioms.
 Require Export ZArithRing.
 Require Import Omega.
 Require Export RealField.
-Require Export LegacyField.
 
 Open Local Scope Z_scope.
 Open Local Scope R_scope.
 
 Implicit Type r : R.
 
-(***************************************************************************)
-(** *     Instantiating Field tactic on reals                              *)
-(***************************************************************************)
-
-(* Legacy Field *)
-Require Export LegacyField.
-Import LegacyRing_theory.
-
-Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
-  split.
-  exact Rplus_comm.
-  symmetry  in |- *; apply Rplus_assoc.
-  exact Rmult_comm.
-  symmetry  in |- *; apply Rmult_assoc.
-  intro; apply Rplus_0_l.
-  intro; apply Rmult_1_l.
-  exact Rplus_opp_r.
-  intros.
-  rewrite Rmult_comm.
-  rewrite (Rmult_comm n p).
-  rewrite (Rmult_comm m p).
-  apply Rmult_plus_distr_l.
-  intros; contradiction.
-Defined.
-
-Add Legacy Field
-R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
-  with minus := Rminus div := Rdiv.
-
 (**************************************************************************)
 (** * Relation between orders and equality                                *)
 (**************************************************************************)
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index db995f3b0..f048faf53 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -397,15 +397,14 @@ Lemma pow_1_even : forall n:nat, (-1) ^ (2 * n) = 1.
 Proof.
   intro; induction  n as [| n Hrecn].
   reflexivity.
-  replace (2 * S n)%nat with (2 + 2 * n)%nat.
+  replace (2 * S n)%nat with (2 + 2 * n)%nat by ring.
   rewrite pow_add; rewrite Hrecn; simpl in |- *; ring.
-  replace (S n) with (n + 1)%nat; [ ring | ring ].
 Qed.
 
 (**********)
 Lemma pow_1_odd : forall n:nat, (-1) ^ S (2 * n) = -1.
 Proof.
-  intro; replace (S (2 * n)) with (2 * n + 1)%nat; [ idtac | ring ].
+  intro; replace (S (2 * n)) with (2 * n + 1)%nat by ring.
   rewrite pow_add; rewrite pow_1_even; simpl in |- *; ring.
 Qed.
 
@@ -425,7 +424,7 @@ Proof.
   intros; induction  n2 as [| n2 Hrecn2].
   simpl in |- *; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ].
   replace (n1 * S n2)%nat with (n1 * n2 + n1)%nat.
-  replace (S n2) with (n2 + 1)%nat; [ idtac | ring ].
+  replace (S n2) with (n2 + 1)%nat by ring.
   do 2 rewrite pow_add.
   rewrite Hrecn2.
   simpl in |- *.