declared ML module ltac_plugin has not been found

[Alizter]

I get the following warnings:

COQDEP coq/theories/Init/Decimal.v
*** Warning: in file coq/theories/Init/Prelude.v, declared ML module numeral_notation_plugin has not been found!
COQDEP coq/theories/Init/Tactics.v
COQDEP coq/theories/Init/Peano.v
COQDEP coq/theories/Init/Logic_Type.v
COQDEP coq/theories/Init/Datatypes.v
COQDEP coq/theories/Init/Logic.v
COQDEP coq/theories/Init/Notations.v
*** Warning: in file coq/theories/Init/Notations.v, declared ML module ltac_plugin has not been found!
COQC coq/theories/Bool/Bool
COQC coq/theories/Init/Notations

How do we get rid of them?

[mikeshulman]

Is this still an issue?

[Alizter]

Yes.

[Alizter]

I'm still getting these warnings with coq 8.11.2. Anybody have any idea how to fix these?

[SkySkimmer]

I think this is a coq bug, coqdep should add the -coqlib we pass to the ML path.