-
Notifications
You must be signed in to change notification settings - Fork 67
Open
Description
I am probably just using this wrong but maybe we could get something better than "Assertion failed" for this error message?
Elpi Tactic abc.
Elpi Accumulate lp:{{
solve G GL.
}}.
Goal forall (x : nat), x = x.
Proof.
intros.
elpi abc ltac_term:(x).
Anomaly "File "src/rocq_elpi_arg_HOAS.ml", line 1107, characters 70-76: Assertion failed."
Please report at http://rocq-prover.org/bugs/.
the tutorial says ltac_term:(v) (for v of type constr or open_constr or uconstr or hyp), and x is a hyp so not sure what i'm doing wrong.
Metadata
Metadata
Assignees
Labels
No labels