aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/Makefile
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-08-31 14:50:59 +0200
committerGuillaume Melquiond2020-11-13 15:14:34 +0100
commitb6fadbf6f08860609961f6dbad8a036346925265 (patch)
treed54fcf732cea3b60ec76b2d0b2c3d938816eb656 /doc/plugin_tutorial/Makefile
parent20c511d4a80c26a54004a9b44b3108669baa86c3 (diff)
Make callback opcodes more generic.
This does not make the code any slower, since Is_coq_array(accu) && Is_uint63(sp[0]) and !Is_accu(accu) && !Is_accu(sp[0]) take the exact same number of tests to pass in the concrete case. In the accumulator case, it takes one more test to fail, but we do not care about the performances then.
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions