strange warning from coqdep

[Casteran]

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]

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]

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