diff options
| author | Pierre-Marie Pédrot | 2018-09-21 13:22:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-19 13:54:47 +0200 |
| commit | d24125537710202cc15a8d6a7352072bd6c77cba (patch) | |
| tree | 7f61942976af89fc074c673f8593784f10331fef /kernel/nativecode.ml | |
| parent | eba0e54f6ecef38b451ef84a978b9ab55699ccf8 (diff) | |
Explicitly merge contexts in side-effect universe handling.
Instead of threading the universe state and making it grow, we make clear
in the signature that the differed side-effects generate constraints to be
added.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions