Converting an Ltac tactic to Proofview.tactic

Developing plugins
1

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?

1 Like
2

There is an example in plugins/setoid_ring/newring.ml. It builds an ist environment using Value.of_constr to encapsulate Constr.ts, and a TacCall to apply the Ltac tactic.

I don’t know how much this is the best way to do though. And, maybe there is already somewhere a macro to do that (@ppedrot would probably know).