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
I would have (naively) expected the do_module
line to be in the with Not_found ->
branch
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)
see also the way Global.end_module and globalize_with_summary work
Maxime Dénès has marked this topic as resolved.
Thanks Gaëtan!
Last updated: May 28 2023 at 13:30 UTC