diff options
| author | Thomas Bauereiss | 2020-01-22 20:43:25 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2020-01-22 20:43:25 +0000 |
| commit | 821779fc44c4af2bed7235925925d24a510f1172 (patch) | |
| tree | 6a99e575b936fde802a31cabbadebf3d938c5340 /src/initial_check.ml | |
| parent | 3199a8954acccbaa4d779c39c6a7ee891e056651 (diff) | |
Preserve effect annotation when realising mappings
Diffstat (limited to 'src/initial_check.ml')
0 files changed, 0 insertions, 0 deletions