search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

declared ML module ltac_plugin has not been found #1134

Open Alizter opened 4 years ago

Alizter commented 4 years ago

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 commented 4 years ago

Is this still an issue?

Alizter commented 4 years ago

Yes.

Alizter commented 4 years ago

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

SkySkimmer commented 4 years ago

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