aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/5550.v
blob: bb1222489a0fa59758c750b889939d0e7b7d3550 (plain)
1
2
3
4
5
6
7
8
9
10
Section foo.

  Variable bar : Prop.
  Variable H : bar.

  Goal bar.
    typeclasses eauto with foobar.
  Qed.

End foo.