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