Pierre-Marie Pédrot (Sep 07 2020 at 12:23): Pierre-Marie Pédrot (Sep 07 2020 at 12:23):Is that me or the rewrite * and autorewrite * variants are not documented?
Pierre-Marie Pédrot (Sep 07 2020 at 12:24):I'm not even sure what these variants do actually.
Pierre-Marie Pédrot (Sep 07 2020 at 12:25):The commit that introduces them is not that helpful either: https://github.com/coq/coq/commit/fa7e44d
Jason Gross (Sep 08 2020 at 01:24):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