Modularization of BinInt, related fixes in the stdlib

 All the functions about Z is now in a separated file BinIntDef,
 which is Included in BinInt.Z. This BinInt.Z directly
 implements ZAxiomsSig, and instantiates derived properties ZProp.

 Note that we refer to Z instead of t inside BinInt.Z,
 otherwise ring breaks later on @eq Z.t

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

1 files changed, 12 insertions, 12 deletions

diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index 4f6332d3d2..55ba0ca1c7 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -59,20 +59,20 @@ Extract Constant N.compare =>
  "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
 
 
-Extract Constant Zplus => "(+)".
-Extract Constant Zsucc => "succ".
-Extract Constant Zpred => "pred".
-Extract Constant Zminus => "(-)".
-Extract Constant Zmult => "( * )".
-Extract Constant Zopp => "(~-)".
-Extract Constant Zabs => "abs".
-Extract Constant Zmin => "min".
-Extract Constant Zmax => "max".
-Extract Constant Zcompare =>
+Extract Constant Z.add => "(+)".
+Extract Constant Z.succ => "succ".
+Extract Constant Z.pred => "pred".
+Extract Constant Z.sub => "(-)".
+Extract Constant Z.mul => "( * )".
+Extract Constant Z.opp => "(~-)".
+Extract Constant Z.abs => "abs".
+Extract Constant Z.min => "min".
+Extract Constant Z.max => "max".
+Extract Constant Z.compare =>
  "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
 
-Extract Constant Z_of_N => "fun p -> p".
-Extract Constant Zabs_N => "abs".
+Extract Constant Z.of_N => "fun p -> p".
+Extract Constant Z.abs_N => "abs".
 
 (** Zdiv and Zmod are quite complex to define in terms of (/) and (mod).
     For the moment we don't even try *)