aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorNickolai Zeldovich2015-07-16 18:31:00 -0400
committerMaxime Dénès2015-09-03 18:11:32 +0200
commit5c060d56a9d94d74cdeca6f6b424306218e81562 (patch)
tree0fefa957d9eee140b55299bfa3d8d4505c230b9c /kernel/cbytecodes.ml
parentc7fd3cb7945bcd385ace06f583d1b57681c8716d (diff)
Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.v
The previous extraction of [Z.div] for Haskell did not properly handle divide-by-zero. Fix it by introducing an explicit [if] statement in the generated Haskell code. Also, introduce a similar extraction rule for [Z.modulo], with the same check for modulo-by-zero.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions