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

summary refs log tree commit diff

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

blob: bb1222489a0fa59758c750b889939d0e7b7d3550 (plain)

Section foo.

  Variable bar : Prop.
  Variable H : bar.

  Goal bar.
    typeclasses eauto with foobar.
  Qed.

End foo.