Hello, I am trying to use (in Coq 8.17) the functions
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
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. *)
Last updated: Nov 29 2023 at 21:01 UTC