aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/6490.v
blob: dcf9ff29edacc7335cdd9c02e009981f46213065 (plain)
1
2
3
4
Inductive Foo (A' := I) (B : Type) := foo : Foo B.

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