(* Testing 8.5 regression with type classes not solving evars
redefined while trying to solve them with the type class mechanism *)
Class A := {}. Axiom foo : forall {ac : A}, bool. Lemma bar (ac : A) : True. Check (match foo as k return foo = k -> True with
| true => _
| false => _ end eq_refl). Abort.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
