diff options
| author | Pierre-Marie Pédrot | 2019-06-25 12:00:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-08 20:47:04 +0200 |
| commit | 75de485c233dd7bbb6301b49e6702eee205977fb (patch) | |
| tree | d5627dfca6f93864945fdfeaad2846ddf30d149c /kernel/safe_typing.ml | |
| parent | 3ce18524834bb9ff7a9ea14c3f1659decb63af76 (diff) | |
Further cleanup following the removal of pure opaque definitions.
We can statically enforce that opaque definitions are always impure by
means of typing, leading to quite a few simplifications.
Diffstat (limited to 'kernel/safe_typing.ml')
0 files changed, 0 insertions, 0 deletions