3 files changed, 0 insertions, 61 deletions
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 3730bcd7f2..2400055aa0 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -187,25 +187,3 @@ rewrite Q2R_inv; auto.
 Qed.
 
 Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl.
-
-Section LegacyQField.
-
-(** In the past, the field tactic was not able to deal with setoid datatypes,
-    so translating from Q to R and applying field on reals was a workaround.
-    See now Qfield for a direct field tactic on Q. *)
-
-Ltac QField := apply eqR_Qeq; autorewrite with q2r_simpl; try field; auto.
-
-(** Examples of use: *)
-
-Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z).
-intros; QField.
-Qed.
-
-Let ex2 : forall x y : Q, ~ y==0 -> (x/y)*y == x.
-intros; QField.
-intro; apply H; apply eqR_Qeq.
-rewrite H0; unfold Q2R; simpl; field; auto with real.
-Qed.
-
-End LegacyQField.
diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
deleted file mode 100644
index 8a62eb8663..0000000000
--- a/theories/Reals/LegacyRfield.v
+++ /dev/null
@@ -1,38 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export Raxioms.
-Require Export LegacyField.
-Import LegacyRing_theory.
-
-Section LegacyRfield.
-
-Open Scope R_scope.
-
-Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
-  split.
-  exact Rplus_comm.
-  symmetry ; apply Rplus_assoc.
-  exact Rmult_comm.
-  symmetry ; 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.
-
-End LegacyRfield.
-
-Add Legacy Field
-R Rplus Rmult 1%R 0%R Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
-  with minus := Rminus div := Rdiv.
diff --git a/theories/Reals/vo.itarget b/theories/Reals/vo.itarget
index 36dd0f56d7..0c8f0b9763 100644
--- a/theories/Reals/vo.itarget
+++ b/theories/Reals/vo.itarget
@@ -8,7 +8,6 @@ Cos_rel.vo
 DiscrR.vo
 Exp_prop.vo
 Integration.vo
-LegacyRfield.vo
 Machin.vo
 MVT.vo
 NewtonInt.vo