test-suite/bugs/closed/4165.v


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.