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
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: Feb 27 2024 at 22:02 UTC