Better visibility of the inductive CompSpec used to specify comparison functions

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

2 files changed, 14 insertions, 13 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 70830ad802..609241d5e8 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -87,6 +87,19 @@ Qed.
 Hint Unfold Qeq Qlt Qle : qarith.
 Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.
 
+Lemma Qcompare_antisym : forall x y, CompOpp (x ?= y) = (y ?= x).
+Proof.
+ unfold "?=". intros. apply Zcompare_antisym.
+Qed.
+
+Lemma Qcompare_spec : forall x y, CompSpec Qeq Qlt x y (x ?= y).
+Proof.
+ intros.
+ destruct (x ?= y) as [ ]_eqn:H; constructor; auto.
+ rewrite Qeq_alt; auto.
+ rewrite Qlt_alt, <- Qcompare_antisym, H; auto.
+Qed.
+
 (** * Properties of equality. *)
 
 Theorem Qeq_refl : forall x, x == x.
diff --git a/theories/QArith/QOrderedType.v b/theories/QArith/QOrderedType.v
index 3d83eac38f..f6f457f654 100644
--- a/theories/QArith/QOrderedType.v
+++ b/theories/QArith/QOrderedType.v
@@ -42,19 +42,7 @@ Module Q_as_OT <: OrderedTypeFull.
  Proof. auto with *. Qed.
 
  Definition le_lteq := Qle_lteq.
-
- Lemma Qcompare_antisym : forall x y, CompOpp (x ?= y) = (y ?= x).
- Proof.
- unfold "?=". intros. apply Zcompare_antisym.
- Qed.
-
- Lemma compare_spec : forall x y, Cmp Qeq Qlt x y (Qcompare x y).
- Proof.
- intros.
- destruct (x ?= y) as [ ]_eqn:H; constructor; auto.
- rewrite Qeq_alt; auto.
- rewrite Qlt_alt, <- Qcompare_antisym, H; auto.
- Qed.
+ Definition compare_spec := Qcompare_spec.
 
 End Q_as_OT.