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 ?
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.
So indeed plugins cannot really do that
in a safe way
Last updated: Dec 05 2023 at 11:01 UTC