Nicolas Magaud (Sep 10 2020 at 11:33): Nicolas Magaud (Sep 10 2020 at 11:33):Inside a plugin I am writing, I try to use the Ocaml function load_vernac from "toplevel/vernac.ml" to load some Coq proof scripts generated by an external tool. I have trouble finding what to put as argument for the argument "state" of the function load_vernac. How do I get the current state (or the empty/initial state) to feed the function with appropriate arguments ?
Emilio Jesús Gallego Arias (Sep 10 2020 at 15:54):Hi @Nicolas Magaud , that's not really a public or stable API, but more specific to toplevel's internals that go back in history. Check for example ccompile as to see how to create a state on that level.
Emilio Jesús Gallego Arias (Sep 10 2020 at 15:56):So indeed plugins cannot really do that
Emilio Jesús Gallego Arias (Sep 10 2020 at 15:58):in a safe way
Last updated: May 31 2023 at 02:31 UTC