···227227228228 It can be set multiple times.
229229230230- Module authors can use its value, which is always a list of module values,
231231- in `imports` or in `submoduleWith`'s `modules` parameter.
230230+ Module authors can use its value in `imports`, in `submoduleWith`'s `modules`
231231+ or in `evalModules`' `modules` parameter, among other places.
232232+232233 Note that `imports` must be evaluated before the module fixpoint. Because
233234 of this, deferred modules can only be imported into "other" fixpoints, such
234235 as submodules.
···441441 It can be set multiple times.
442442 </para>
443443 <para>
444444- Module authors can use its value, which is always a list of
445445- module values, in <literal>imports</literal> or in
446446- <literal>submoduleWith</literal>’s
447447- <literal>modules</literal> parameter. Note that
448448- <literal>imports</literal> must be evaluated before the
449449- module fixpoint. Because of this, deferred modules can only
450450- be imported into <quote>other</quote> fixpoints, such as
451451- submodules.
444444+ Module authors can use its value in
445445+ <literal>imports</literal>, in
446446+ <literal>submoduleWith</literal><quote>s
447447+ <literal>modules</literal> or in
448448+ <literal>evalModules</literal></quote>
449449+ <literal>modules</literal> parameter, among other places.
450450+ </para>
451451+ <para>
452452+ Note that <literal>imports</literal> must be evaluated
453453+ before the module fixpoint. Because of this, deferred
454454+ modules can only be imported into <quote>other</quote>
455455+ fixpoints, such as submodules.
452456 </para>
453457 <para>
454458 One use case for this type is the type of a