Hi, sorry to trouble you. According to the documentation, tactics are built from atomic tactics and tactic expressions(like the Ltac language). The are several languages for tactic expressions, like Ltac1, Ltac2... But what is the language for atomic? Ltac1?
I think the manual refers to that certain tactics are implemented directly in OCaml, like auto
in tactics/auto.ml
. If this is the case, the tactic is "atomic".
May be a bit more subtle, if you look at the definition of the tacexpr
type
Last updated: Oct 13 2024 at 01:02 UTC