diff options
| author | Matthieu Sozeau | 2015-12-02 17:35:25 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-12-02 17:35:25 +0100 |
| commit | 42c68765690710b16f3e878bf1d914eaa75d8291 (patch) | |
| tree | 102a5d644805781300fdfac0b5577f2c658e3b37 /kernel/nativecode.ml | |
| parent | c62eb0470975c9b5960a49a90b49b4aa191efd1c (diff) | |
Fix bug #4444: Next Obligation performed after a Section opening was
using the wrong context.
This is very bad style but currently unavoidable, at least we don't
throw an anomaly anymore.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions