Chantal Keller (Apr 20 2021 at 14:34): Chantal Keller (Apr 20 2021 at 14:34):Hello
Is there a way to call a Ltac tactic in a vernac command? I would like to do something like:
Foo bar.
which first applies a Ltac tactic on bar returning bar', then applies a vernacular command (written in OCaml) on bar'.
Thanks!
Emilio Jesús Gallego Arias (Apr 20 2021 at 16:51):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.
Chantal Keller (Apr 21 2021 at 07:02):Thank you Emilio. So there is a way to get in OCaml a tactic written in Ltac and to apply it?
Emilio Jesús Gallego Arias (Apr 21 2021 at 11:43):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: Oct 03 2023 at 02:34 UTC