evar1.v « failure « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

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).