Is it possible to check if the sent coq statement is a tactic with serapi?

[brando90]

Is it possible to check if the sent coq statement is a tactic with serapi?

[ejgallego]

That's doable but (as often with Coq) a bit tricky, as Coq language is extensible by plugins, and even Ltac1 is a plugin, the check will be necessarily partial.

But if you restrict yourself to ssreflect and ltac, yes, it should be possible by checking the AST of the Coq statement.