aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-05-02 15:42:10 +0200
committerGuillaume Melquiond2016-05-02 15:42:10 +0200
commitd7a9fea94772971a52d04f9f266fe6d5e25cd40e (patch)
tree381752564133f3b612b2c1f0b914a02360b3c5e3 /kernel
parentbd5da52c6c625cb4559dd92051384383473ecb1b (diff)
Avoid infinite loop/stack overflow when using "simpl nomatch" (bug #4576).
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.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions