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

summary refs log tree commit diff

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

blob: 39ba1903697ffc7847043f036d3e7314840c0d81 (plain)

Require Import Setoid.

Definition block A (a : A) := a.

Goal forall A (a : A), block Type nat.
Proof.
Fail reflexivity.