Stream: Ltac2

Topic: Issues with calling Ltac1 tactic notations


view this post on Zulip Michael Soegtrop (Mar 10 2021 at 09:24):

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.

view this post on Zulip Pierre-Marie Pédrot (Mar 10 2021 at 09:25):

You have to be explicit when passing values between Ltac1 and Ltac2 quotations.

view this post on Zulip Pierre-Marie Pédrot (Mar 10 2021 at 09:25):

It is mentioned in the doc, I believe.

view this post on Zulip Pierre-Marie Pédrot (Mar 10 2021 at 09:26):

(The reason for that is that the notion of bound variable in Ltac1 is really weird.)

view this post on Zulip Michael Soegtrop (Mar 10 2021 at 09:32):

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: Jan 31 2023 at 10:01 UTC