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 :)

`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. *)
```

Thank you @Gaëtan Gilbert ! How can I use `run`

or `apply`

correctly then?

```
Require Import Ltac2.Ltac2.
Goal True -> True -> True.
Proof.
Ltac1.run ltac1val:(intros x).
Ltac1.apply ltac1val:(fun H => intros H) [Ltac1.of_ident ident:(y)] (fun tac => Ltac1.run tac).
```

Great ! Thank you again !!

Louise Dubois de Prisque has marked this topic as resolved.

Last updated: May 18 2024 at 08:40 UTC