Is that me or the
rewrite * and
autorewrite * variants are not documented?
I'm not even sure what these variants do actually.
The commit that introduces them is not that helpful either: https://github.com/coq/coq/commit/fa7e44d
Oh, neat! I didn't realize this existed. I think this solves a problem that I've worked around in the past (in fact, I think the
* behavior should be the default (perhaps guarded by a compatibility flag)). Here's an example where it matters:
Axiom foo : forall x, x = 1 -> 2 * x = 2. Goal forall x y, x = 1 -> 2 * y = 2 * x. intros. Fail rewrite foo by assumption. (* The command has indeed failed with message: No such assumption. *) Fail rewrite !foo by assumption. (* The command has indeed failed with message: No such assumption. *) Fail progress rewrite ?foo by assumption. (* The command has indeed failed with message: Failed to progress. *) rewrite *foo by assumption. (* success *)
In fact, I reported this as https://github.com/coq/coq/issues/4976, Sam reported a related issue at https://github.com/coq/coq/issues/7672 explicitly mentioning
rewrite *, and perhaps the commit was originally a fix for https://github.com/coq/coq/issues/1933 ?
Last updated: May 28 2023 at 16:30 UTC