Gaëtan Gilbert (Feb 22 2022 at 11:36): Gaëtan Gilbert (Feb 22 2022 at 11:36):Why do we have .mllib files in plugins/* and vernac/? are they used for anything?
Enrico Tassi (Feb 22 2022 at 12:34):Hum, coqdep?
Gaëtan Gilbert (Feb 22 2022 at 12:36):right
I think the vernac/ one ise really useless though
Emilio Jesús Gallego Arias (Feb 22 2022 at 12:40):Yes we need to get rid of the coqdep stuff for that, eventually
Last updated: Feb 05 2023 at 20:03 UTC