Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

strange warning from coqdep #56

Open
Casteran opened this issue Sep 23, 2020 · 2 comments
Open

strange warning from coqdep #56

Casteran opened this issue Sep 23, 2020 · 2 comments

Comments

@Casteran
Copy link
Member

Hi,
I am writing a library which uses paramcoq (installed with opam).
At compile-time, I get a warning:
*** Warning: in file ./power/Addition_Chains.v, declared ML module paramcoq has not been found!

Happily, the rest of the compilation works well.
Is there a way to say to coqdep that paramcoq is used, like a kind of Require ... (although the directory user-contrib/Param/ doesn't contain any .v ) ?

Pierre

@Zimmi48
Copy link
Member

Zimmi48 commented Sep 23, 2020

The usual recommendation for plugin authors is indeed to provide a .v file even though it may only contain the Declare ML Module command.

@ejgallego
Copy link
Contributor

That's likely a bug on the way coq makefile class coqdep

This was referenced Aug 23, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants