blob: f988539d62c2b09fa192d69da99d17763733fd7a (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* 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).
|
