summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4576.v
blob: 2c643ea779fc092bf781a9eca54a9bd59504b287 (plain)
1
2
3
Definition foo := O.
Arguments foo : simpl nomatch.
Timeout 1 Eval cbn in id foo.