diff options
| author | Pierre-Marie Pédrot | 2016-08-31 11:32:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-31 11:45:41 +0200 |
| commit | 12268bef28dea57fdbe29dc87d26ef453ad5cfed (patch) | |
| tree | 9c4088cd2c3d966bd5769522e21eb173de885468 /kernel/nativecode.ml | |
| parent | 3da141c5dfed50e1b9a4ad5421b4abacdcc23dae (diff) | |
Fix bug #5043: [Admitted] lemmas pick up section variables.
We add a flag Keep Admitted Variables that allows to recover the legacy
v8.4 behaviour of admitted lemmas. The statement of such lemmas did not
depend on the current context variables.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions