diff options
| author | Christopher Pulte | 2016-10-19 15:49:18 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-10-19 15:49:18 +0100 |
| commit | 019ce013a1274cd9c1af13c5f5d33f444de85d88 (patch) | |
| tree | 03d0c1b9afdaa39343a2eb78b73658d6d8533913 /src/pretty_print.ml | |
| parent | c5d020885780addd197cb83b0fb9996b564b409f (diff) | |
remove effect list from instruction type
Diffstat (limited to 'src/pretty_print.ml')
0 files changed, 0 insertions, 0 deletions