blob: 8226622670b5162dcae8375c8ceaf66c95f9d356 (
plain)
1
2
3
4
5
6
|
Inductive T := Foo : T.
Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
Axiom a1 : match b with Foo => f end = f.
Axiom a2 : match b with Foo => f b end = f b.
Hint Rewrite a1 : bar.
Hint Rewrite a2 : bar.
|
