Coq-Equations icon indicating copy to clipboard operation
Coq-Equations copied to clipboard

Exception on invalid syntax

Open TobiasKappe opened this issue 2 years ago • 0 comments

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/.

TobiasKappe avatar Aug 24 '22 22:08 TobiasKappe