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: Oct 13 2024 at 01:02 UTC