diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/ExtrOcamlZBigInt.v | 6 | ||||
| -rw-r--r-- | plugins/extraction/ExtrOcamlZInt.v | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index 12607b3ad2..27fce8eab9 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -75,13 +75,13 @@ 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). +(** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod). For the moment we don't even try *) (** Test: Require Import ZArith NArith. Extraction "/tmp/test.ml" - Pplus Ppred Pminus Pmult Pcompare Npred Nminus Ndiv Nmod Ncompare - Zplus Zmult BinInt.Zcompare Z_of_N Zabs_N Zdiv.Zdiv Zmod. + Pos.add Pos.pred Pos.sub Pos.mul Pos.compare N.pred N.sub N.div N.modulo N.compare + Z.add Z.mul Z.compare Z.of_N Z.abs_N Z.div Z.modulo. *) diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v index 55ba0ca1c7..9566c0186b 100644 --- a/plugins/extraction/ExtrOcamlZInt.v +++ b/plugins/extraction/ExtrOcamlZInt.v @@ -74,7 +74,7 @@ Extract Constant Z.compare => 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). +(** Z.div and Z.modulo are quite complex to define in terms of (/) and (mod). For the moment we don't even try *) |