diff options
| author | Arnaud Spiwack | 2014-10-16 14:28:01 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-16 14:35:34 +0200 |
| commit | ce260a0db279ce09dda70e079ae3c35b49f05ec4 (patch) | |
| tree | 21f409a6874f9f390c86d3ce6f5d4b14a49d7bdc /kernel/nativecode.ml | |
| parent | 025c4f63b28671a24bd6c46f9b23a3dad76fd179 (diff) | |
Refine: proper scoping of the future goals.
In my first attempt I just dropped all future goals before starting a refinement. This was done for simplicity but is incorrect in general. In this version the future goals which are not introduced by the particular instance of refine are kept for future use.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions