Thanks!
That made it work.
Julin Shaji has marked this topic as resolved.
The loader file at https://github.com/coq-community/coq-plugin-template/blob/v8.16/theories/MyPlugin.v
Still uses that legacy syntax (hadn't even known before that there was such a syntax).
Should that be changed?
And how could a _CoqProject
to use the plugin look like? For the plugin-template.
Julin Shaji said:
Thanks!
That made it work.
I'm still confused as to which name should appear where. The relation between name in dune-project or opam file or dune file, etc.
Tried to recreate the template with a different name, couldn't make it work. So sticking to template coq-my-plugin
now.
If I use the legacy loading way, I can Import the plugin interactively from editor.
But if I change the Declare ML Module
to remove the prefix associated with legacy loading, I can't use it from editor.
I guess it's due to something that needs to changed in the _CoqProject file?
Last updated: Oct 13 2024 at 01:02 UTC