The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I believe Matthieu Sozeau is working on getting the setoid_rewrite machinery to handle relations in Type, and also (I think?) dependent/heterogeneous relations.  It will hopefully be in Coq 8.5.  Have you looked at how setoid_rewriting is implemented with typeclass resolution?

-Jason

On Thu, Feb 27, 2014 at 4:21 PM, Rui Baptista <rpgcbaptista AT gmail.com> wrote:

It works if I use

Hint Extern 1 => apply A1 : CompatHints.

Hint Extern 1 => apply A2 : CompatHints.

Hint Extern 1 => apply A3 : CompatHints.

Hint Extern 1 => apply A4 : CompatHints.

Hint Extern 1 => apply A5 : CompatHints.

Hint Extern 1 => apply A6 : CompatHints.

Hint Extern 1 => apply A7 : CompatHints.

Hint Extern 1 => apply A8 : CompatHints.

Hint Extern 1 => apply A9 : CompatHints.

Hint Extern 1 => apply A10 : CompatHints.

Hint Extern 1 => apply A11 : CompatHints.

instead of

Hint Resolve A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 : CompatHints.

But it's kind of slow, and I'm forced to use

Global Opaque not.

so it doesn't unfold not. Also, it prefers to use compatibility with universal quantification instead of implication.

I used refine (iff_backwards _ _ _ _) when I should have used refine (iff_forwards _ _ _ _).