I ran into trouble with
rewrite works though). Here are minimal examples (Coq 8.13.2 as well as
Definition f (n : nat) : nat := S n. Lemma f_spec (n : nat) : f n = S n. Proof. reflexivity. Qed. Lemma test_f (n : nat) : S n = f n. Proof. Fail rewrite f_spec. (* Tactic generated a subgoal identical to the original goal. *) Abort.
Ah, possibly this is exactly #14132. Currently, @Ali Caglayan possibly the issue is mislabeled as
kind: performance. This looks like a critical rewriting issue.
Sorry for mislabelling, I've marked it as a bug now.
Last updated: Jan 29 2023 at 05:03 UTC