1 files changed, 2 insertions, 95 deletions
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index f9aa3e50..2d45d537 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -6,99 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Qring.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
-
-Require Export Ring.
-Require Export QArith_base.
-
-(** * A ring tactic for rational numbers *)
-
-Definition Qeq_bool (x y : Q) :=
-  if Qeq_dec x y then true else false.
-
-Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y.
-Proof.
-  intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
-  intros _ H; inversion H.
-Qed.
-
-Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
-Proof.
-  constructor.
-  exact Qplus_0_l.
-  exact Qplus_comm.
-  exact Qplus_assoc.
-  exact Qmult_1_l.
-  exact Qmult_comm.
-  exact Qmult_assoc.
-  exact Qmult_plus_distr_l.
-  reflexivity.
-  exact Qplus_opp_r.
-Qed.
-
-Ltac isQcst t :=
-  match t with
-  | inject_Z ?z => isZcst z
-  | Qmake ?n ?d =>
-    match isZcst n with
-      true => isPcst d
-    | _ => false
-    end
-  | _ => false
-  end.
-
-Ltac Qcst t :=
-  match isQcst t with
-    true => t
-    | _ => NotConstant
-  end.
-
-Add Ring Qring : Qsrt (decidable Qeq_bool_correct, constants [Qcst]).
-(** Exemple of use: *)
-
-Section Examples. 
-
-Let ex1 : forall x y z : Q, (x+y)*z ==  (x*z)+(y*z).
-  intros.
-  ring.
-Qed.
-
-Let ex2 : forall x y : Q, x+y == y+x.
-  intros. 
-  ring.
-Qed.
-
-Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
-  intros.
-  ring.
-Qed.
-
-Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
- ring.
-Qed.
-
-Let ex5 : 1+1 == 2#1.
-  ring.
-Qed.
-
-Let ex6 : (1#1)+(1#1) == 2#1.
-  ring.
-Qed.
-
-Let ex7 : forall x : Q, x-x== 0#1.
-  intro.
-  ring.
-Qed.
-
-End Examples.
-
-Lemma Qopp_plus : forall a b,  -(a+b) == -a + -b.
-Proof.
-  intros; ring.
-Qed.
-
-Lemma Qopp_opp : forall q, - -q==q.
-Proof.
-  intros; ring.
-Qed.
+(*i $Id: Qring.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
 
+Require Export Qfield.