I noticed (by accident) that the behavior of the `specialize`

tactic changed in Coq 8.14:

```
Lemma test (X : nat -> Prop) (H : forall n, X n) (H' : forall n, X n -> X (S n)) : True.
Proof.
specialize (H 5) as J%H'.
```

In 8.13, this produces the following goal:

```
X : nat -> Prop
H' : forall n : nat, X n -> X (S n)
J : X 6
============================
True
```

In 8.14, it instead produces:

```
X : nat -> Prop
H : X 6
H' : forall n : nat, X n -> X (S n)
============================
True
```

Notice there is no `J`

even though the `as`

pattern says to call the result `J`

.

Is this deliberate? the changelog does not seem to mention it (I did Ctrl-F 'specialize').

Arguably `specialize ... as`

is weird, but just ignoring the name in the pattern seems like a bug to me -- in particular since without the `%H'`

, the name is still honored. (Cc @Hugo Herbelin because `%`

patterns seem relevant.)

looks like it was not deliberate: https://github.com/coq/coq/issues/15244

It is a bug. Thanks for reporting. This is issue #15244, fixed by #15245.

Last updated: Jun 23 2024 at 23:01 UTC