The Coq manual says
tacarg, there is an overlap between
qualid as a direct tactic argument and
qualid as a particular case of
I can not fully understand this sentence. The tactic
split is denoted by
tacarg. What does
split belong to? A direct tactic argument or a term?
First, there is a
split tactic and a
split term. The
split tactic is not a valid
split is not a valid
Ltac foo tac := tac.
Ltac bar := foo split.
Goal True /\ True.
Fail foo split.
I’ve found that sentence under https://coq.inria.fr/refman/proof-engine/ltac.html#syntax.
In that context,
term means Gallina term, and the
split tactic is not a Gallina term.
If you invoke the
split tactic directly,
split is a tactic and not a
tacarg; if you pass
split as argument to another tactic, then it’s a tactic argument.
That sentence is pretty weird, but https://coq.github.io/doc/v8.12/refman/proof-engine/ltac.html#grammar-token-tactic-arg gives the grammar directly.
PS: Please link to the source next time, it wasn’t easy to find.