Stream: Ltac2

Topic: Use of Ltac1.run, Ltac1.apply and Ltac1.of_ident

Louise Dubois de Prisque (Sep 18 2023 at 14:44):

Hello, I am trying to use (in Coq 8.17) the functions Ltac1.run and Ltac1.apply from Ltac2. But I am doing something wrong and I don't understand the problem. Here is a minimal example:

Goal True -> True.
Fail Ltac1.run (Ltac1.of_ident (@intros)).

(* The command has indeed failed with message:
Expression does not evaluate to a tactic. *)

Ltac1.apply (Ltac1.of_ident (@intros)) [] Ltac1.run.

(*The command has indeed failed with message:
 Variable F should be bound to a tactic. *)

In the first example, the error message is strange because intros is indeed a tactic, and not a Ltac1 value. So maybe the problem leads in my use of Ltac1.of_ident ?
In the second example, the error message is difficult to understand, maybe it is linked to a similar problem.

If you have some working examples on how to use these functions, that would be really helpful !

Thank you in advance for your help :)

Gaëtan Gilbert (Sep 18 2023 at 15:07):

of_ident produces a ltac1 value which is the given ident
What you want is something which resolves the ident to the ltac1 it is bound to in some environment. I don't think we provide such an API currently.

Basically you're getting the same result as

Tactic Notation "foo" ident(x) := x.

Goal True.
  foo intros.
(* Expression does not evaluate to a tactic. *)

Last updated: Nov 29 2023 at 21:01 UTC