What's the difference between ssr rewrite's matching algorithm and vanilla Coq's? Interestingly, ssr's `rewrite !`

is linear in the size of the goal when there are no occurrences of the head symbol (and every constant that appears in the goal is either an `Axiom`

or an `Inductive`

), while `autorewrite`

and Coq's `rewrite !`

are quadratic in the size of the goal. (I'll be reporting an issue about this shortly.

reported at https://github.com/coq/coq/issues/12600

Last updated: Oct 13 2024 at 01:02 UTC