Ssreflect Users Discussion List

[Georges Gonthier <>]

(forwarding a private reply to the list...)

However, note that if H is parametrised, then rewrite {2}H may behave 
differently than rewrite -> H at 2, because Ssreflect always determines the 
parameters based on the leftmost match, and only uses the occurrence numbers 
to distinguish between identical subterms; you are meant to use the redex 
pattern feature to select a specific term. Coq simply gives you the second 
match, which leads to more fragile scripts, and is rather ill-defined when 
you need multiple occurrences (again, Coq will rewrite simultaneously 
different instances, but the ocurrence counting does not take into account 
overlapping or nested redexes.).

Georges

-----Original Message-----
From: Chantal KELLER [] 
Sent: 12 September 2009 11:37
To: Bas Spitters
Cc: 
Subject: Re: Ssreflect and corn

Bas Spitters a écrit :
> Thanks!
> 
> 
> How do I translate:
> rewrite -> H at 1.
> 
> 
> to ssr?
> 
> 
> Bas


Hello,

You can translate it as follows:
rewrite {1}H.

-- 
Chantal KELLER