You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
relies on the fact that the record Verdi.Net.network is defined in some file other than GhostSimulations.v (in this case, in the file Net.v). This is an instance of coq/coq#3523.
Suggested fixes:
- destruct net.+ destruct net as [? nwState].
concludes.
destruct nwState.
or
destruct net.
concludes.
- destruct nwState.+ let nwState := match goal with H : data |- _ => H end in destruct nwState.
The text was updated successfully, but these errors were encountered:
I'd suggest whichever one is more robust to future changes: the former is more robust to the changes in the specific types of the fields and the presence of new context variables, while the latter is more robust to changes in field ordering. Which of these seems more important to be robust to? (Said another way, which better captures the essence of the proof: "destruct the second field of net a second time" or "destruct the first thing in the context of type data"?)
(If they seem equally relevant, I'd lean towards the first one, since it's fewer characters and probably easier for humans to read.)
My bug minimizer cannot fully minimize the example at coq/coq#14798 (comment) because
verdi/core/GhostSimulations.v
Lines 86 to 88 in 002da48
Verdi.Net.network
is defined in some file other thanGhostSimulations.v
(in this case, in the fileNet.v
). This is an instance of coq/coq#3523.Suggested fixes:
or
The text was updated successfully, but these errors were encountered: