3062.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/bugs/closed/3062.v

blob: a7b5fab03ec1b1e0e0150440d34fdc8dd69c3b8d (plain)

Lemma foo : forall x y:nat, x < y -> False.
Proof.
  intros x y H.
  induction H as [ |?y ?y ?y].
Abort.