Ryan Brott (May 27 2021 at 04:37): Ryan Brott (May 27 2021 at 04:37):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 coqc).
Théo Zimmermann (May 27 2021 at 07:20):@Ryan Brott That's a bug, so could you open an issue with details on how to reproduce and your configuration?
Last updated: Apr 19 2024 at 19:02 UTC