Simplification of Numbers, mainly thanks to Include

 - No more nesting of Module and Module Type, we rather use Include.
 - Instead of in-name-qualification like NZeq, we use uniform
   short names + modular qualification like N.eq when necessary.
 - Many simplification of proofs, by some autorewrite for instance
 - In NZOrder, we instantiate an "order" tactic.
 - Some requirements in NZAxioms were superfluous: compatibility
   of le, min and max could be derived from the rest.
 - NMul removed, since it was containing only an ad-hoc result for
   ZNatPairs, that we've inlined in the proof of mul_wd there.
 - Zdomain removed (was already not compiled), idea of a module
   with eq and eqb reused in DecidableType.BooleanEqualityType.
 - ZBinDefs don't contain any definition now, migrate it to ZBinary.

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

1 files changed, 0 insertions, 59 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
deleted file mode 100644
index 500dd9f535..0000000000
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ /dev/null
@@ -1,59 +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        *)
-(************************************************************************)
-(*                      Evgeny Makarov, INRIA, 2007                     *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-Require Import Bool.
-Require Export NumPrelude.
-
-Module Type ZDomainSignature.
-
-Parameter Inline Z : Set.
-Parameter Inline Zeq : Z -> Z -> Prop.
-Parameter Inline Zeqb : Z -> Z -> bool.
-
-Axiom eqb_equiv_eq : forall x y : Z, Zeqb x y = true <-> Zeq x y.
-Instance eq_equiv : Equivalence Zeq.
-
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with Z.
-Notation "x == y" := (Zeq x y) (at level 70) : IntScope.
-Notation "x # y" := (~ Zeq x y) (at level 70) : IntScope.
-
-End ZDomainSignature.
-
-Module ZDomainProperties (Import ZDomainModule : ZDomainSignature).
-Open Local Scope IntScope.
-
-Instance Zeqb_wd : Proper (Zeq ==> Zeq ==> eq) Zeqb.
-Proof.
-intros x x' Exx' y y' Eyy'.
-apply eq_true_iff_eq.
-rewrite 2 eqb_equiv_eq, Exx', Eyy'; auto with *.
-Qed.
-
-Theorem neq_sym : forall n m, n # m -> m # n.
-Proof.
-intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
-Qed.
-
-Theorem ZE_stepl : forall x y z : Z, x == y -> x == z -> z == y.
-Proof.
-intros x y z H1 H2; now rewrite <- H1.
-Qed.
-
-Declare Left Step ZE_stepl.
-
-(* The right step lemma is just transitivity of Zeq *)
-Declare Right Step (@Equivalence_Transitive _ _ eq_equiv).
-
-End ZDomainProperties.
-
-