test-suite/bugs/closed/bug_9451.v


1
2
3
4
5
6
7
8

Goal False.
cut True.
assert False.
evar (x : True).
let v := open_constr:(_) in idtac. all: exfalso; clear.
Optimize Proof.
(* Error: Anomaly "grounding a non evar-free term" *)
Abort All.