diff options
author | 2007-10-04 13:02:03 +0000 | |
---|---|---|
committer | 2007-10-04 13:02:03 +0000 | |
commit | 2cc806b646cd15bd98c48df8612abd2360f9e93e (patch) | |
tree | 5b9723ec305d6b24d239daa289d2e18cea9365ea /test-suite/bugs | |
parent | e19ab99ea5b440dad9f80a57d18637f4d2d49811 (diff) |
Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10172 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/bugs')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1718.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1718.v b/test-suite/bugs/closed/shouldsucceed/1718.v new file mode 100644 index 000000000..715fa9419 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1718.v @@ -0,0 +1,9 @@ +(* lazy delta unfolding used to miss delta on rels and vars (fixed in 10172) *) + +Check + let g := fun _ => 0 in + fix f (n : nat) := + match n with + | 0 => g f + | S n' => 0 + end. |