Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix bug #3920: eapply masks an hypothesis name. | 2016-08-30 | |
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. |