Maxime Dénès (Mar 08 2022 at 12:55): 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
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
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)
Gaëtan Gilbert (Mar 08 2022 at 13:00):see also the way Global.end_module and globalize_with_summary work
Notification Bot (Mar 23 2022 at 09:06):Maxime Dénès has marked this topic as resolved.
Maxime Dénès (Mar 23 2022 at 09:06):Thanks Gaëtan!
Last updated: Dec 07 2023 at 09:01 UTC