Modularization of BinNat + fixes of stdlib

 A sub-module N in BinNat now contains functions add (ex-Nplus),
 mul (ex-Nmult), ... and properties.

 In particular, this sub-module N directly instantiates NAxiomsSig
  and includes all derived properties NProp.

 Files Ndiv_def and co are now obsolete and kept only for compat

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

2 files changed, 20 insertions, 20 deletions

diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index fd8ad6d77..c73451e5c 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -48,18 +48,18 @@ Extract Constant Pos.compare =>
 Extract Constant Pos.compare_cont =>
  "fun x y c -> Big.compare_case c Lt Gt x y".
 
-Extract Constant Nplus => "Big.add".
-Extract Constant Nsucc => "Big.succ".
-Extract Constant Npred => "fun n -> Big.max Big.zero (Big.pred n)".
-Extract Constant Nminus => "fun n m -> Big.max Big.zero (Big.sub n m)".
-Extract Constant Nmult => "Big.mult".
-Extract Constant Nmin => "Big.min".
-Extract Constant Nmax => "Big.max".
-Extract Constant Ndiv =>
+Extract Constant N.add => "Big.add".
+Extract Constant N.succ => "Big.succ".
+Extract Constant N.pred => "fun n -> Big.max Big.zero (Big.pred n)".
+Extract Constant N.sub => "fun n m -> Big.max Big.zero (Big.sub n m)".
+Extract Constant N.mul => "Big.mult".
+Extract Constant N.min => "Big.min".
+Extract Constant N.max => "Big.max".
+Extract Constant N.div =>
  "fun a b -> if Big.eq b Big.zero then Big.zero else Big.div a b".
-Extract Constant Nmod =>
+Extract Constant N.modulo =>
  "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b".
-Extract Constant Ncompare => "Big.compare_case Eq Lt Gt".
+Extract Constant N.compare => "Big.compare_case Eq Lt Gt".
 
 Extract Constant Zplus => "Big.add".
 Extract Constant Zsucc => "Big.succ".
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index 013695772..4f6332d3d 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -46,16 +46,16 @@ Extract Constant Pos.compare_cont =>
  "fun x y c -> if x=y then c else if x<y then Lt else Gt".
 
 
-Extract Constant Nplus => "(+)".
-Extract Constant Nsucc => "succ".
-Extract Constant Npred => "fun n -> max 0 (n-1)".
-Extract Constant Nminus => "fun n m -> max 0 (n-m)".
-Extract Constant Nmult => "( * )".
-Extract Constant Nmin => "min".
-Extract Constant Nmax => "max".
-Extract Constant Ndiv => "fun a b -> if b=0 then 0 else a/b".
-Extract Constant Nmod => "fun a b -> if b=0 then a else a mod b".
-Extract Constant Ncompare =>
+Extract Constant N.add => "(+)".
+Extract Constant N.succ => "succ".
+Extract Constant N.pred => "fun n -> max 0 (n-1)".
+Extract Constant N.sub => "fun n m -> max 0 (n-m)".
+Extract Constant N.mul => "( * )".
+Extract Constant N.min => "min".
+Extract Constant N.max => "max".
+Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b".
+Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b".
+Extract Constant N.compare =>
  "fun x y -> if x=y then Eq else if x<y then Lt else Gt".