Stream: Coq devs & plugin devs

Topic: ✔ Effect of `Require` on already loaded lib

view this post on Zulip Maxime Dénès (Mar 08 2022 at 12:55):

Does anybody know why we seem to load objects of library even when they are already loaded? https://github.com/coq/coq/blob/master/vernac/declaremods.ml#L1027

view this post on Zulip Maxime Dénès (Mar 08 2022 at 12:56):

I would have (naively) expected the do_module line to be in the with Not_found -> branch

view this post on Zulip Gaëtan Gilbert (Mar 08 2022 at 12:59):

probably because in

Module M.
Require Bla.
End M.

when ending M Bla is not removed from the global env but the non logical objects are removed (or rather their effects on the summary are reset)

view this post on Zulip Gaëtan Gilbert (Mar 08 2022 at 13:00):

see also the way Global.end_module and globalize_with_summary work

view this post on Zulip Notification Bot (Mar 23 2022 at 09:06):

Maxime Dénès has marked this topic as resolved.

view this post on Zulip Maxime Dénès (Mar 23 2022 at 09:06):

Thanks Gaëtan!

Last updated: May 28 2023 at 13:30 UTC