Hi
In SMTCoq, I use the Micromega plugin at the OCaml level. I used to refer to it by Micromega_plugin. ...
but when porting to Coq-8.16 I get Error: Unbound module Micromega_plugin
. How can I refer to it? Do I need to add something in some lookup path?
Thanks!
Sounds like the move to findlib for loading plugins, you can probably take inspiration on the overlay pull requests listed in the initial pull request: https://github.com/coq/coq/pull/15220
You need to instruct ocamlfind
to find it, e.g., with -package coq-core.plugins.micromega
.
Many thanks to both of you, that helped me solve my problem, and also understand better what to put in my own -generate-meta-for-package
and Declare ML Module
.
By the way, I do not find the documentation really clear about pkg
and foo
.
Chantal Keller has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC