diff options
| author | Matthieu Sozeau | 2015-09-24 10:51:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:11 +0200 |
| commit | 89cf845e1653c2f9b274d413561f10b7019d4858 (patch) | |
| tree | 21ab0e740b90ad2886a7271019813096433b126e /kernel/nativecode.ml | |
| parent | b969b459021fe70272baa85e83c12268baf13836 (diff) | |
discriminate: Do fresh_global in the right env in presence of side-effects.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions