diff options
author | 2015-12-02 17:35:25 +0100 | |
---|---|---|
committer | 2015-12-02 17:35:25 +0100 | |
commit | 42c68765690710b16f3e878bf1d914eaa75d8291 (patch) | |
tree | 102a5d644805781300fdfac0b5577f2c658e3b37 /test-suite/bugs/opened/3304.v | |
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 'test-suite/bugs/opened/3304.v')
0 files changed, 0 insertions, 0 deletions