bug_4893.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

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

blob: 1b1ca7c1084385c47ed03883ade80bd65c0c6e2f (plain)

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