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
Is this deliberate? the changelog does not seem to mention it (I did Ctrl-F 'specialize').
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: Feb 08 2023 at 23:03 UTC