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