You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
The text was updated successfully, but these errors were encountered:
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
The text was updated successfully, but these errors were encountered: