The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi Pierre,

I think you are missing the coercion :> for op_m, similarly to what is
done for op_equiv.

Best,

Stéphane

On Wed, Feb 17, 2010 at 11:59 AM, Pierre Casteran
<pierre.casteran AT labri.fr>
 wrote:
> Hello,
>
>  I've got some problem trying to use rewrite in some deep occurrence of a
> subterm.
>
>  In the following example (attached file), the rewrite fails, whilst an
> iterated application
> of op_m succeeds. What is failing in the class declaration for having a
> "rewrite H" ok ?
>
> Pierre
>
>
>
>
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06