diff options
author | 2016-08-30 17:37:27 +0200 | |
---|---|---|
committer | 2016-08-30 17:57:25 +0200 | |
commit | 44ada644ef50563aa52cfcd7717d44bde29e5a20 (patch) | |
tree | f887873a5db55840367610d130914c8c18c56495 /plugins/micromega/Lra.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/Lra.v')
0 files changed, 0 insertions, 0 deletions