Jean-Christophe Léchenet
Jean-Christophe Léchenet
I think we need a dedicated error message when the bank is empty. Having an error explaining that it conflicts with nothing is really confusing.
Fixed by #313.
Fixed by #313.
The issue is fixed and a beta release of apron (that I suppose contains the fix) has just been released on opam. Maybe it is worth testing that this fixes...
I encountered the same problem (with mutual fixpoints inside a section).
I encountered also this problem on CoqIDE. I also observe that `Elpi Export` makes some proofs fail with an anomaly when compiling with `-async-proofs on`.
Coq 8.18 and 8.19. Both have the issue.
But strangely, depending on the setting, the bug happens always or really rarely. I don't manage to understand the pattern. I mean, the minimized version always fail. But in Jasmin,...
To reproduce, as mentioned in the first message of this issue. ``` From elpi Require Import elpi. Elpi Command bla. Elpi Export bla. Goal True. Proof. reflexivity. Qed. ``` `coqc...
``` derive.param1_trivial generates illtyped term: Illegal application: The term "is_Toto" of type "forall H : unit, is_unit H -> forall (n : nat) (Pn : is_nat n) (H0 : is_zero...