From b101806c92d776926227239568e3638e1dbc88db Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Sun, 13 Jul 2025 17:12:24 -0700
Subject: [PATCH] doc: Add description for `CompactCoreState`

---
 Pantograph/Serial.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean
index a7ae3d0..a06c89c 100644
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@@ -101,7 +101,7 @@ def environmentUnpickle (path : System.FilePath) (background? : Option Environme
   return (← resurrectEnvironment distilled background?, region)
 
 
-open Lean.Core in
+/-- `CoreM`'s state, with information irrelevant to pickling masked out -/
 structure CompactCoreState where
   -- env             : Environment
   nextMacroScope  : MacroScope     := firstFrontendMacroScope + 1