diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-30 17:37:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-30 17:57:25 +0200 |
| commit | 44ada644ef50563aa52cfcd7717d44bde29e5a20 (patch) | |
| tree | f887873a5db55840367610d130914c8c18c56495 /plugins/micromega/Lqa.v | |
| parent | dea5e8a7ecb2120cccd2d2631ddbf892e99bffda (diff) | |
Fix bug #3920: eapply masks an hypothesis name.
The problem came from the fact that the legacy beta-reduction occurring
after a rewrite was wrongly applied to the side-conditions of the
rewriting step. We restrict it to the correct goal in this patch.
Diffstat (limited to 'plugins/micromega/Lqa.v')
0 files changed, 0 insertions, 0 deletions