I was working with Ltac2 on creating some simple tactics, and I ran into the following problem: let us assume that we have some Ltac2 tactics
Ltac2 Notation "Tactic name" s(constr) := ... Ltac2 Notation "Tactic name" s(ident) "one more word" t(constr) := ...
When calling the above tactics, Ltac2 does not always recognize which tactic I am calling. For instance, if I want to call the first tactic and just write
Tactic name s.
s that makes sense in a
goal, I receive an error that there are more arguments needed (as it assumes that I am calling the second tactic, and I think this happens because it is the last one that is compiled).
Is it possible to circumvent this without changing the names of the tactics?