The Coq mailing list

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

Hi,

It seems there is no variant of enough with respect to assumptions.
Could you use

replace a with b in H' |-.

instead ?

Regards,

--
Laurent

On 7/18/20 10:11 AM, Chris Dams wrote:
> Dear all,
> 
> Coqide says that cutrewrite is deprecated. The docs say that I should
> use the enough tactic instead. So I can do 'enough (a = b) as ->'
> instead of 'cutrewrite (a = b)'. This works but what do I do when I
> would want to do 'cutrewrite (a = b) in H'. I.e., use cutrewrite to
> rewrite something in a hypothesis?
> 
> Regards,
> Chris