Ssreflect Users Discussion List

[Maxime Dénès <>]

Indeed, declaring any PER as an instance of RewriteRelation solves the 
problem (it's done only for Equivalence in RelationClasses).

I wonder why Coq's rewrite accepts this without the instance declaration 
then, but I'm fine with this.

Thank you Enrico!

Maxime.

On 26/11/2012 13:47, Enrico Tassi wrote:
> On Mon, Nov 26, 2012 at 01:30:51PM +0100, Maxime Dénès wrote:
> > Hi Enrico!
> >
> > Thanks for your lightning-fast answer.
> >
> > The constant Class_setoid.Classes.RelationClasses.RewriteRelation does
> I guess I wanted to say Classes.RelationClasses.RewriteRelation
>
> > What is still surprising is that when the relation is declared as an
> > Equivalence instead of a PER, this test seems to succeed.
> Hum, can you check that PER is a RewriteRelation?
> What Rewrite.is_applied_rewrite_relation does is calling the
> type classes resolution mecanism.
>
> Ciao