Fix bug #1899: no more strange notations for Qge and Qgt

In fact, Qge and Ggt disappear, and we only leave notations for > and >=
that map directly to Qlt and Qle. 

We also adopt the same approach for BigN, BigZ, BigQ.

By the way, various clean-up concerning Zeq_bool, Zle_bool and similar
functions for Q. 



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

1 files changed, 9 insertions, 18 deletions

diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index 2e51ef973..5373c1db3 100644
--- a/theories/QArith/Qfield.v
+++ b/theories/QArith/Qfield.v
@@ -14,24 +14,9 @@ Require Import NArithRing.
 
 (** * field and ring tactics 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.
-
-Lemma Qeq_bool_complete : forall x y : Q, x==y -> Qeq_bool x y = true.
-Proof.
-  intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
-Qed.
-
-Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq.
+Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
 Proof.
   constructor.
-  constructor.
   exact Qplus_0_l.
   exact Qplus_comm.
   exact Qplus_assoc.
@@ -41,6 +26,12 @@ Proof.
   exact Qmult_plus_distr_l.
   reflexivity.
   exact Qplus_opp_r.
+Qed.
+
+Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq.
+Proof.
+  constructor.
+  exact Qsrt.
   discriminate.
   reflexivity.
   intros p Hp.
@@ -83,8 +74,8 @@ Ltac Qpow_tac t :=
   end.
 
 Add Field Qfield : Qsft 
- (decidable Qeq_bool_correct, 
-  completeness Qeq_bool_complete,
+ (decidable Qeq_bool_eq, 
+  completeness Qeq_eq_bool,
   constants [Qcst], 
   power_tac Qpower_theory [Qpow_tac]).