summaryrefslogtreecommitdiff
path: root/src/bytecode_util.ml
diff options
context:
space:
mode:
authorBrian Campbell2018-06-28 11:42:12 +0100
committerBrian Campbell2018-06-28 11:42:27 +0100
commit19e7e5c6e15a3b9e0038d0bb83f78e576ad0adc5 (patch)
treeb68d0aa43e9c1affdba4ad9a6e504d4953b02f5b /src/bytecode_util.ml
parent807bd2a5e9ff3cb96bd83b0bb675977e4860447f (diff)
Deduplicate arguments for different constructors in undefined fns
Makes the generated undefined functions smaller, easier to read, and avoids excessive memory usage in Coq (e.g., for large AST types).
Diffstat (limited to 'src/bytecode_util.ml')
0 files changed, 0 insertions, 0 deletions