From d2bd5d87d23d443f6e41496bdfe5f8e82d675634 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:59 +0000 Subject: 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 --- plugins/extraction/ExtrOcamlZBigInt.v | 26 +++++++++++++------------- plugins/extraction/ExtrOcamlZInt.v | 24 ++++++++++++------------ 2 files changed, 25 insertions(+), 25 deletions(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index c73451e5c..12607b3ad 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -61,19 +61,19 @@ Extract Constant N.modulo => "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b". Extract Constant N.compare => "Big.compare_case Eq Lt Gt". -Extract Constant Zplus => "Big.add". -Extract Constant Zsucc => "Big.succ". -Extract Constant Zpred => "Big.pred". -Extract Constant Zminus => "Big.sub". -Extract Constant Zmult => "Big.mult". -Extract Constant Zopp => "Big.opp". -Extract Constant Zabs => "Big.abs". -Extract Constant Zmin => "Big.min". -Extract Constant Zmax => "Big.max". -Extract Constant Zcompare => "Big.compare_case Eq Lt Gt". - -Extract Constant Z_of_N => "fun p -> p". -Extract Constant Zabs_N => "Big.abs". +Extract Constant Z.add => "Big.add". +Extract Constant Z.succ => "Big.succ". +Extract Constant Z.pred => "Big.pred". +Extract Constant Z.sub => "Big.sub". +Extract Constant Z.mul => "Big.mult". +Extract Constant Z.opp => "Big.opp". +Extract Constant Z.abs => "Big.abs". +Extract Constant Z.min => "Big.min". +Extract Constant Z.max => "Big.max". +Extract Constant Z.compare => "Big.compare_case Eq Lt Gt". + +Extract Constant Z.of_N => "fun p -> p". +Extract Constant Z.abs_N => "Big.abs". (** Zdiv and Zmod are quite complex to define in terms of (/) and (mod). For the moment we don't even try *) diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index 4f6332d3d..55ba0ca1c 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 "(+)". -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 "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 *) -- cgit v1.2.3