aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/evar1.v
blob: 2b6fe765452e3127ecb11290cbbd1a5b3464b3d4 (plain)
1
2
3
(* This used to succeed by producing an ill-typed term in v8.2 *)

Fail Lemma u: forall A : Prop, (exist _ A A) = (exist _ A A).