summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorBrian Campbell2018-09-04 18:36:18 +0100
committerBrian Campbell2018-09-04 18:36:18 +0100
commitcff8eb8a6febc26a2742f5c88b933f5441727b29 (patch)
tree2e5b4af35fae440b6bd27f3ca42cbec0e32f4502 /lib
parenta51ad0a3afb65af3209f67ace7defd24bf42c26d (diff)
Add a rewrite to minimise the number of functions marked as recursive
Particularly useful when execute has been split up (e.g., on RISC-V). Only enabled on Coq for now.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions