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?
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
Many thanks to both of you, that helped me solve my problem, and also understand better what to put in my own
Declare ML Module.
By the way, I do not find the documentation really clear about
Chantal Keller has marked this topic as resolved.
Last updated: Dec 07 2023 at 09:01 UTC