Legacy Ring and Legacy Field migrated to contribs

 One slight point to check someday : fourier used to
 launch a tactic called Ring.polynom in some cases.
 It it crucial ? If so, how to replace with the setoid_ring
 equivalent ?

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

1 files changed, 0 insertions, 22 deletions

diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 3730bcd7f..2400055aa 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.