aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4165.v
blob: 8e0a62d35c313babf0681d8083cff53335185af0 (plain)
1
2
3
4
5
6
7
Lemma foo : True.
Proof.
pose (fun x : nat => (let H:=true in x)) as s.
match eval cbv delta [s] in s with
| context C[true] =>
  let C':=context C[false] in pose C' as s'
end.