aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ShowProof.v
blob: 19822ac50e0e4d3e4409cfb93801f186b6dae3c6 (plain)
1
2
3
4
5
6
7
(* Was #4524 *)
Definition foo (x : Type) : True /\ True.
Proof.
split.
- exact I.
  Show Proof. (* Was not finding an evar name at some time *)
Abort.