aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3461.v
blob: 1b625e6a15ae48ff9183454fd99663c47417ad0f (plain)
1
2
3
4
5
Lemma foo (b : bool) :
  exists x : nat, x = x.
Proof.
eexists. 
Fail eexact (eq_refl b).