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)).
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: Nov 29 2023 at 06:01 UTC