aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3920.v
AgeCommit message (Collapse)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2016-08-30Fix bug #3920: eapply masks an hypothesis name.Pierre-Marie Pédrot
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.