I've been debugging a loop in repeat match goal with | H : _ /\ _ |- _ => destruct H end
for a while. I already know I can work around it with repeat match goal with | H : _ /\ _ |- _ => revert H; case; intros end
but I would like to understand under which circumstances destruct
behaves this way. Does anybody happen to know?
If H
is a section variable, it will not be cleared. I do not know if there are other cases.
H
is not a section variable but there might have been a section variable called H
that got renamed to make room for the new H
.
I wonder if the logic to detect if something is a section variable knows that section variables can be renamed
It does not..
Section Test.
Context (H : True).
Goal True /\ True -> True.
Proof.
intros H'. rename H into H0. rename H' into H.
Fail Timeout 1 repeat match goal with [ H : _ /\ _ |- _ ] => destruct H end.
@Guillaume Melquiond thank you. You solved the mystery!
Reported in https://github.com/coq/coq/issues/18858
Last updated: Oct 13 2024 at 01:02 UTC