Stream: Coq users

Topic: SLF anomaly


view this post on Zulip 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).

view this post on Zulip 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: Feb 01 2023 at 13:03 UTC