What do people think about this snippet:

```
Section S.
Variables x y : nat.
Definition sx := 1 + x.
Lemma t : sx = 1+y.
Fail clear x.
rename x into x'.
pose y as x.
unfold sx.
unfold x.
reflexivity.
Fail Qed.
```

Would this be considered a bug? It is a bit inconsistent that `clear`

errors, but `rename`

does not.

It looks to me like `rename`

does not type check its result, while `clear`

does perform the type check.

I believe related to https://github.com/coq/coq/issues/6773

Yes, this seems highly related indeed. Thanks for the reference

Last updated: Sep 09 2024 at 06:02 UTC