path: root/test-suite/bugs/closed/4893.v

Goal True.
evar (P: Prop).
assert (H : P); [|subst P]; [exact I|].
let T := type of H in not_evar T.