Stream: Miscellaneous

Topic: load_vernac


view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 10 2020 at 15:56):

So indeed plugins cannot really do that

view this post on Zulip Emilio Jesús Gallego Arias (Sep 10 2020 at 15:58):

in a safe way


Last updated: Mar 28 2024 at 10:01 UTC