I just started working through volume 6 of Software Foundations in Coq version 8.13.0, and I get
Anomaly "Uncaught exception Failure("hd")." on the
xwp tactic in the first proof in
Basic.v. Strangely, I can only reproduce in CoqIde (not with
@Ryan Brott That's a bug, so could you open an issue with details on how to reproduce and your configuration?
Last updated: Feb 01 2023 at 13:03 UTC