diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 5a9488ed65..b4c5662fd7 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -141,7 +141,10 @@ structure EnvironmentHeader where imports : Array Import := #[] /-- Compacted regions for all imported modules. Objects in compacted memory regions do no require any memory management. -/ regions : Array CompactedRegion := #[] - /-- Name of all imported modules (directly and indirectly). -/ + /-- + Name of all imported modules (directly and indirectly). + The index of a module name in the array equals the `ModuleIdx` for the same module. + -/ moduleNames : Array Name := #[] /-- Module data for all imported modules. -/ moduleData : Array ModuleData := #[]