I am trying to package a Coq development so that it can be installed with
opam and made visible to Coq. It does not happen.
opam, for example
opam install coq-equationsworks and makes
opam install . --working-dirto install my development. It succeeds.
~/.opam/default/.opam-switch/build. I expect it to appear under
~/.opam/default/libas other developments I installed previously.
Require Import Example.results in
Error: Unable to locate library Example. (While searching for a .vos file.).
What am I doing wrong?
I think you need some -Q or -R to apply to your files for installation to work
ie libraries that have no prefix in their name may have issues
-Q . nice solved the issue.
Last updated: Feb 08 2023 at 23:03 UTC