Tacarg in Ltac

Using Rocq
1

The Coq manual says
“In tacarg, there is an overlap between qualid as a direct tactic argument and qualid as a particular case of term.”

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?

2

First, there is a split tactic and a split term. The split tactic is not a valid tacarg.

First, the split is not a valid tacarg.

Ltac foo tac := tac.
Ltac bar := foo split.
Goal True /\ True. 
Fail foo split.
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.

1 Like