diff options
Diffstat (limited to 'plugins/extraction/ExtrOcamlZBigInt.v')
| -rw-r--r-- | plugins/extraction/ExtrOcamlZBigInt.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index 12607b3ad..27fce8eab 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. *) |