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: Dec 01 2023 at 07:01 UTC