diff options
| author | Pierre-Marie Pédrot | 2019-06-05 10:35:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-11 16:59:07 +0200 |
| commit | e753855167e5629775b604128c6efc9d58ee626c (patch) | |
| tree | 7abdebb08679b76a80cf9d1a36f05b91a538c223 /kernel/nativevalues.ml | |
| parent | 3d162ca9095ff9299be5cc8847636a36b8e49f1e (diff) | |
Remove the side-effect role from the kernel.
We move the role data into the evarmap instead.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions