From d7a9fea94772971a52d04f9f266fe6d5e25cd40e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 2 May 2016 15:42:10 +0200
Subject: 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.
---
 test-suite/bugs/closed/4576.v | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 test-suite/bugs/closed/4576.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4576.v b/test-suite/bugs/closed/4576.v
new file mode 100644
index 0000000000..2c643ea779
--- /dev/null
+++ b/test-suite/bugs/closed/4576.v
@@ -0,0 +1,3 @@
+Definition foo := O.
+Arguments foo : simpl nomatch.
+Timeout 1 Eval cbn in id foo.
-- 
cgit v1.2.3