max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove hack

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-03 18:29:18 -08:00
parent bd2243d978
commit 52a27c08cf
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Elab/Frontend.lean
View file

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