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

1 files changed, 0 insertions, 9 deletions

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.