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

diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 40f08356b..4cc867898 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -20,14 +20,14 @@ Require Import Cyclic31.
 Require Import NSig.
 Require Import NSigNAxioms.
 Require Import NMake.
-Require Import NSub.
+Require Import NProperties.
 
 Module BigN <: NType := NMake.Make Int31Cyclic.
 
 (** Module [BigN] implements [NAxiomsSig] *)
 
 Module Export BigNAxiomsMod := NSig_NAxioms BigN.
-Module Export BigNSubPropMod := NSubPropFunct BigNAxiomsMod.
+Module Export BigNPropMod := NPropFunct BigNAxiomsMod.
 
 (** Notations about [BigN] *)
 
@@ -38,7 +38,7 @@ Bind Scope bigN_scope with bigN.
 Bind Scope bigN_scope with BigN.t.
 Bind Scope bigN_scope with BigN.t_.
 
-Notation Local "0" := BigN.zero : bigN_scope. (* temporary notation *)
+Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
 Infix "+" := BigN.add : bigN_scope.
 Infix "-" := BigN.sub : bigN_scope.
 Infix "*" := BigN.mul : bigN_scope.