diff options
| author | Pierre-Marie Pédrot | 2018-09-16 21:02:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-19 13:54:47 +0200 |
| commit | eba0e54f6ecef38b451ef84a978b9ab55699ccf8 (patch) | |
| tree | 547bee7dff9fe03db00bf1b75f005f3ad6b2deaf /kernel/nativecode.mli | |
| parent | 6ab9a8088394b710ae0b9f6d5711d2fe0509419f (diff) | |
Move side-effect typing into Safe_env.
This reduces the attack surface of the API, as actually there is only a back
and forth between the two modules, and side-effects validity certificates are
intuitively nothing more than safe environments.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions