test-suite/bugs/closed/bug_2854.v


1
2
3
4
5
6
7
8
9

Section foo.
  Let foo := Type.
  Definition bar : foo -> foo := @id _.
  Goal False.
    subst foo.
    Fail pose bar as f.
    (* simpl in f. *)
  Abort.
End foo.