Stream: Coq devs & plugin devs

Topic: .mllib?


view this post on Zulip Gaëtan Gilbert (Feb 22 2022 at 11:36):

Why do we have .mllib files in plugins/* and vernac/? are they used for anything?

view this post on Zulip Enrico Tassi (Feb 22 2022 at 12:34):

Hum, coqdep?

view this post on Zulip Gaëtan Gilbert (Feb 22 2022 at 12:36):

right
I think the vernac/ one ise really useless though

view this post on Zulip 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