Zcompare.destr_zcompare subsumed by case Z.compare_spec

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

2 files changed, 3 insertions, 18 deletions

diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index d4db2c66d..33267a518 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -68,15 +68,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Proof.
  intros x; rewrite N.spec_0; generalize (N.spec_pos x). romega.
  Qed.
-(*
- Lemma if_fun_commut : forall A B (f:A->B)(b:bool) a a',
- f (if b then a else a') = if b then f a else f a'.
- Proof. now destruct b. Qed.
-
- Lemma if_fun_commut' : forall A B C D (f:A->B)(b:{C}+{D}) a a',
- f (if b then a else a') = if b then f a else f a'.
- Proof. now destruct b. Qed.
-*)
+
+ Ltac destr_zcompare := case Z.compare_spec; intros ?H.
+
  Ltac destr_eqb :=
   match goal with
    | |- context [Z.eqb ?x ?y] =>
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 49ab619bc..25925a25c 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -19,15 +19,6 @@ Local Open Scope Z_scope.
 (***************************)
 (** * Comparison on integers *)
 
-Ltac destr_zcompare :=
- match goal with |- context [Z.compare ?x ?y] =>
-  let H := fresh "H" in
-  case_eq (Z.compare x y); intro H;
-   [generalize (Z.compare_eq _ _ H); clear H; intro H |
-    change (x<y)%Z in H |
-    change (x>y)%Z in H ]
- end.
-
 Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt.
 Proof Z.gt_lt_iff.