Suppose I have tactic TAC declared in a *.v file by Ltac TAC args := … I want to access it in a plugin at the OCaml level as a Proofview.tactic. What is the best way to do this?
In particular, if TAC takes a constr argument, how do I convert it to Proofview.tactic so that I can feed it a Constr.t or EConstr.t? This is the case I’m most interested in. If there are no arguments or the arguments are identifiers, then I know how to do this using Tacenv.locate_tactic and Tacinterp.eval_tactic (I’m not sure if it’s the preferred solution). But I have not been able to figure out from Coq sources how to convert an Ltac-level tactic taking a constr argument into an OCaml-level function taking a Constr.t and returning a unit Proofview.tactic. Is this even possible?