diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 8db5f6778c..85241a96aa 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -113,6 +113,10 @@ structure Environment where
   Recall that a Leah file has a header where previously compiled modules can be imported.
   Each imported module has a unique `ModuleIdx`.
   Many extensions use the `ModuleIdx` to efficiently retrieve information stored in imported modules.
+
+  Remark: this mapping also contains auxiliary constants, created by the code generator, that are **not** in
+  the field `constants`. These auxiliary constants are invisible to the Lean kernel and elaborator.
+  Only the code generator uses them.
   -/
   const2ModIdx : HashMap Name ModuleIdx
   /--