The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 7/8/20 10:37 PM, Agnishom Chattopadhyay wrote:
> Does loading ssreflect change the standard behaviour of tacticals like
> in/by/with/etc? This is a problem since a large part of my proof script
> uses things like rewrite H in H0.

yes it does, it is explained in

https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html

in particular rewrite has a slighy different semantics
but has some extra capability like a powerful pattern selection.

If you want to do use the standard rewrite, just add <- in front the
first theorem. So rewrite ->H in H0 should work.

--
Laurent