6490.v « closed « bugs « test-suite - coq - the Coq proof assistant

about summary refs log tree commit diff homepage

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

blob: dcf9ff29edacc7335cdd9c02e009981f46213065 (plain)

Inductive Foo (A' := I) (B : Type) := foo : Foo B.

Goal Foo True. dtauto. Qed.
Goal Foo True. firstorder. Qed.