It is written in the Mathematical Components book that `rewrite {}H`

should rewrite H and then erase it from the context. For some reason, this never works for me. Only `move {H}`

works. Any explanation or way to fix it?...

```
Lemma L (x y : nat) P : x = y -> P x.
Proof.
move=> h. rewrite {}h.
```

gives

```
x, y : nat
P : nat -> Type
============================
P y
```

What version of Coq/ssr are you using?

Is `H`

a section variable? (cause these cannot be cleared)

@Enrico Tassi @Pierre-Yves Strub Could it be that it does not work with `by rewrite`

? Your example works, but for instance

```
Lemma L (x y : nat) (P : nat -> Prop) : x = y -> P x -> (P y /\ P y).
Proof.
move=> h hPx. split. by rewrite -{}h.
```

returns a context with h still in it, so `{}`

did not change anything. I think the few times I have tried to use it and it failed, it wasn't a section variable, but it must have been with a `by rewrite`

...

In your example, `by`

is closing the current goal. What you see is hence your second goal where `h`

has not be cleared.

Yes of course, that's right. It must have been the same in my other issues. Thank you very much for clarifying this to me!

Last updated: Mar 03 2024 at 15:01 UTC