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: Mar 03 2024 at 16:02 UTC