What is the motivation for adding the constraint of not opening any 
other files?
You will need to open the interface of M to discover its dependencies at 
one point or another.

On 16/07/2026 at 17:19, K wrote :
> Is iterating over the typexpr the right or reasonable way of 
> uncovering that transitive dependency (on type N.t specifically rather 
> than on the module N in its entirety) without recourse to opening any 
> other file?
>
> On Thu, 16 Jul 2026 at 13:07, Florian Angeletti <octa@polychoron.fr> 
> wrote:
>
>     In your example, `N` will be a dependency of `M` and thus a
>     transitive
>     dependency of the current module.
>