diff options
author | 2017-03-20 18:04:54 +0100 | |
---|---|---|
committer | 2017-03-20 18:04:54 +0100 | |
commit | cd87eac3757d8925ff4ba7dee85efadb195153a3 (patch) | |
tree | bb16605711673d8f4ed851059c82509a6a66fec7 /checker/modops.ml | |
parent | dbbc4da0e52567325d74128dccd1b54760cb970d (diff) | |
parent | 76c263b5eceac313ac2cdd3a3e7e2961876d3e31 (diff) |
Merge PR#430: make `emit' tail recursive
Diffstat (limited to 'checker/modops.ml')
0 files changed, 0 insertions, 0 deletions