The Coq mailing list

[Laurence Rideau <Laurence.Rideau AT inria.fr>]

On 07/30/2014 07:26 PM, Xavier Leroy wrote:
> On 29/07/14 16:28, Enrico Tassi wrote:
> > Let me add that there is no good reason for the tactic to fail here.
> > If "list ..." and "sf" are convertible then they are the very same term.
> Hear, hear!
>
> > In the implementation of the rewrite tactic that is part of ssreflect
> > the conversion relation is taken into account.
> Good to know.  Maybe I should defect to the other side :-)

tu veux de l'aide?

on peut t'aider à passer du  bon côté de la force (ouarf!!)
Bonne journée
Amitiés
laurence