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.
Last updated: Feb 01 2023 at 16:03 UTC