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, 10 insertions, 10 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index f7c423ebb..6e8ca37ca 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -11,7 +11,7 @@
 (*i $Id$ i*)
 
 Require Export BigN.
-Require Import ZMulOrder.
+Require Import ZProperties.
 Require Import ZSig.
 Require Import ZSigZAxioms.
 Require Import ZMake.
@@ -21,7 +21,7 @@ Module BigZ <: ZType := ZMake.Make BigN.
 (** Module [BigZ] implements [ZAxiomsSig] *)
 
 Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
-Module Export BigZMulOrderPropMod := ZMulOrderPropFunct BigZAxiomsMod.
+Module Export BigZPropMod := ZPropFunct BigZAxiomsMod.
 
 (** Notations about [BigZ] *)
 
@@ -32,7 +32,7 @@ Bind Scope bigZ_scope with bigZ.
 Bind Scope bigZ_scope with BigZ.t.
 Bind Scope bigZ_scope with BigZ.t_.
 
-Notation Local "0" := BigZ.zero : bigZ_scope.
+Local Notation "0" := BigZ.zero : bigZ_scope.
 Infix "+" := BigZ.add : bigZ_scope.
 Infix "-" := BigZ.sub : bigZ_scope.
 Notation "- x" := (BigZ.opp x) : bigZ_scope.
@@ -93,13 +93,13 @@ Lemma BigZring :
  ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
 Proof.
 constructor.
-exact Zadd_0_l.
-exact Zadd_comm.
-exact Zadd_assoc.
-exact Zmul_1_l.
-exact Zmul_comm.
-exact Zmul_assoc.
-exact Zmul_add_distr_r.
+exact add_0_l.
+exact add_comm.
+exact add_assoc.
+exact mul_1_l.
+exact mul_comm.
+exact mul_assoc.
+exact mul_add_distr_r.
 exact sub_opp.
 exact add_opp.
 Qed.