ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType

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

1 files changed, 0 insertions, 60 deletions

diff --git a/theories/ZArith/ZOrderedType.v b/theories/ZArith/ZOrderedType.v
deleted file mode 100644
index 570e2a4d6f..0000000000
--- a/theories/ZArith/ZOrderedType.v
+++ /dev/null
@@ -1,60 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import BinInt Zcompare Zorder Zbool ZArith_dec
- Equalities Orders OrdersTac.
-
-Local Open Scope Z_scope.
-
-(** * DecidableType structure for binary integers *)
-
-Module Z_as_UBE <: UsualBoolEq.
- Definition t := Z.
- Definition eq := @eq Z.
- Definition eqb := Zeq_bool.
- Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
-End Z_as_UBE.
-
-Module Z_as_DT <: UsualDecidableTypeFull := Make_UDTF Z_as_UBE.
-
-(** Note that the last module fulfills by subtyping many other
-    interfaces, such as [DecidableType] or [EqualityType]. *)
-
-
-(** * OrderedType structure for binary integers *)
-
-Module Z_as_OT <: OrderedTypeFull.
- Include Z_as_DT.
- Definition lt := Zlt.
- Definition le := Zle.
- Definition compare := Zcompare.
-
- Instance lt_strorder : StrictOrder Zlt.
- Proof. split; [ exact Zlt_irrefl | exact Zlt_trans ]. Qed.
-
- Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Zlt.
- Proof. repeat red; intros; subst; auto. Qed.
-
- Definition le_lteq := Zle_lt_or_eq_iff.
- Definition compare_spec := Zcompare_spec.
-
-End Z_as_OT.
-
-(** Note that [Z_as_OT] can also be seen as a [UsualOrderedType]
-   and a [OrderedType] (and also as a [DecidableType]). *)
-
-
-
-(** * An [order] tactic for integers *)
-
-Module ZOrder := OTF_to_OrderTac Z_as_OT.
-Ltac z_order := ZOrder.order.
-
-(** Note that [z_order] is domain-agnostic: it will not prove
-    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
-