I sometimes have issues with calling Ltac1 tactic notations. An example is this (which requires coq-interval):
Require Import Interval.Tactic.
Require Import Ltac2.Ltac2.
Ltac2 wrap_interval_intro (goal : constr) :=
ltac1:(interval_intro ($goal)).
I get Unbound value goal
which I don't understand.
You have to be explicit when passing values between Ltac1 and Ltac2 quotations.
It is mentioned in the doc, I believe.
(The reason for that is that the notion of bound variable in Ltac1 is really weird.)
Ah yes - I was reading here (https://coq.inria.fr/refman/proof-engine/ltac2.html#variable-binding), but I should have been reading this: (https://coq.inria.fr/refman/proof-engine/ltac2.html#ltac1-from-ltac2). Thanks!
Last updated: Oct 13 2024 at 01:02 UTC