diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-31 11:32:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-31 11:45:41 +0200 |
| commit | 12268bef28dea57fdbe29dc87d26ef453ad5cfed (patch) | |
| tree | 9c4088cd2c3d966bd5769522e21eb173de885468 /test-suite | |
| 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 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/5043.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5043.v b/test-suite/bugs/closed/5043.v new file mode 100644 index 000000000..4e6a0f878 --- /dev/null +++ b/test-suite/bugs/closed/5043.v @@ -0,0 +1,8 @@ +Unset Keep Admitted Variables. + +Section a. + Context (x : Type). + Definition foo : Type. + Admitted. +End a. +Check foo : Type. |