Coq-Equations
Coq-Equations copied to clipboard
Exception on invalid syntax
The following code triggers an exception on my machine, running Coq 8.15.2 and Equations 1.3+8.15:
From Equations Require Import Equations.
Equations foo: bool := {
|}.
Notice the extra pipe before the closing brace.
This is the exception:
Anomaly "Uncaught exception Failure("hd")."
Please report at http://coq.inria.fr/bugs/.