summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/2854.v
blob: 14aee17ff0de14230a47b64942e4db901db9d373 (plain)
1
2
3
4
5
6
7
Section foo.
  Let foo := Type.
  Definition bar : foo -> foo := @id _.
  Goal False.
    subst foo.
    Fail pose bar as f.
    (* simpl in f. *)