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