Ssreflect Users Discussion List

[Robbert Krebbers <>]

Dear Emilio,

Thanks for your reply.

On 01/13/2016 01:16 PM, Emilio Jesús Gallego Arias wrote:
> However it has some particularities, as your next example shows:
>
> > >rewrite H1 in H2.
> > >(* Error: tampering with discharged assumptions of "in" tactical *)
> This may be avoided using:
>
> > >rewrite H1 in H2 *.
> The manual does a better job than I could ever do in explaining "in *".
From the ref man:

  The operation described by tactic is
  performed in the facts listed in ident +
  and in the goal if a * ends the list.

I do not necessarily want the rewrite to be performed in the goal as 
well, so always using * seems not to be the solution.

As Assia remarked here 
https://github.com/math-comp/math-comp/issues/16#issuecomment-171295569 
, it is probably a bug.

Best,

Robbert