Is there a way to call a Ltac tactic in a vernac command? I would like to do something like:
which first applies a Ltac tactic on
bar', then applies a vernacular command (written in OCaml) on
Hi @Chantal Keller , if you are willing to use >= 8.13 and to write you command on OCaml too, you can use the
Declare.Proof.start API, then call the tactic, see the docs https://coq.github.io/doc/master/api/coq-core/Declare/Proof/index.html
That will give you the "proof state", which is required for tactics to run; then you have
Declare.Proof.by and some other helpers. But indeed, it is unfortunately a quite heavy operation these days yet, in particular tactics can do a lot of stuff [universes, side-effect constants, etc...] that you need to reconcile after the tactic has ran; we are trying to much improve the API so hopefully something like Coq 8.15 feels a much better to use.
Thank you Emilio. So there is a way to get in OCaml a tactic written in Ltac and to apply it?
Yup, you should be able to do
ltac -> Proofview.tactic so you can use
Declare.Proof.by , what's the provenance of the ltac snippet?
Last updated: Jan 29 2023 at 01:02 UTC