git.iko.soy/Idris-dev
on master help sign in
Preserve bound var info across implicitness changes
144dfcfDavid Raymond Christiansen
src/Idris/REPL.hs+1−1
compare with master
unifiedsplit
@@ -447,7 +447,7 @@ runIdeSlaveCommand id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =
447ideSlaveForceTermImplicits :: Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
447ideSlaveForceTermImplicits :: Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()
448ideSlaveForceTermImplicits id bnd impl tm =
448ideSlaveForceTermImplicits id bnd impl tm =
449 do ist <- getIState
449 do ist <- getIState
450− let expl = annotate (AnnTerm [] tm)
450+ let expl = annotate (AnnTerm bnd tm)
451 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })
451 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })
452 bnd [] (idris_infixes ist)
452 bnd [] (idris_infixes ist)
453 (delab ist tm))
453 (delab ist tm))