From dadfe84c1571220d13e25bf23e81ebcbd6be9b14 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 25 Sep 2022 14:06:07 -0700
Subject: [PATCH] doc: update `const2ModIdx` docstring

---
 src/Lean/Environment.lean | 4 ++++
 1 file changed, 4 insertions(+)

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
   /--