aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4576.v
Commit message (Collapse)AuthorAge
* Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).Gravatar Guillaume Melquiond2016-05-02
When encountering a "simpl nomatch" constant, the reduction machinery tries to unfold it. If the subsequent partial reduction does not produce any match construct, it keeps going from the reduced term. Unfortunately, the reduced term has been refolded in the meantime, which means that some of the previous reduction steps have been canceled, thus causing an infinite loop. This patch delays the refolding till the very end, so that reduction always progresses. Disclaimer: I have no idea what I am doing here. The patch compiles the standard library and the test suite properly, so hopefully they contain enough tests to exercise the reduction machinery.