From 52a27c08cf06a87def8d2aeec56029542b3154ee Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Jan 2020 18:29:18 -0800 Subject: [PATCH] chore: remove hack --- src/Init/Lean/Elab/Frontend.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Elab/Frontend.lean b/src/Init/Lean/Elab/Frontend.lean index cd8db204fd..b760921370 100644 --- a/src/Init/Lean/Elab/Frontend.lean +++ b/src/Init/Lean/Elab/Frontend.lean @@ -79,7 +79,7 @@ open Frontend def IO.processCommands (parserCtx : Parser.ParserContextCore) (parserStateRef : IO.Ref Parser.ModuleParserState) (cmdStateRef : IO.Ref Command.State) : IO Unit := do ps ← parserStateRef.get; cmdPosRef ← IO.mkRef ps.pos; -EIO.adaptExcept (fun (ex : Empty) => unreachable!) $ -- TODO: compiler support for Empty.rec is missing +EIO.adaptExcept (fun (ex : Empty) => Empty.rec _ ex) $ processCommands { commandStateRef := cmdStateRef, parserStateRef := parserStateRef, cmdPosRef := cmdPosRef, parserCtx := parserCtx } def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do