I ran into trouble with `rewrite`

(`ssreflect`

's `rewrite`

works though). Here are minimal examples (Coq 8.13.2 as well as `master`

):

```
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: Jun 15 2024 at 05:01 UTC