Make prover respect showimplicits from IState
commit94c4cf83b2281c2a722114273ce0263d01e44bf4
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateFri 31 Jan 2014, 19:16 (13 years ago)
parent9a926d5
src/Idris/Prover.hs+3−2
@@ -99,8 +99,9 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = d
9999 prettyAssumptions env <> line <>
100100 prettyGoal (zip (assumptionNames env) (repeat False)) ty
101101 where
102− -- XXX
103− tPretty bnd t = pprintPTerm True bnd $ delab ist t
102+ showImplicits = opt_showimp (idris_options ist)
103+
104+ tPretty bnd t = pprintPTerm showImplicits bnd $ delab ist t
104105
105106 assumptionNames :: Env -> [Name]
106107 assumptionNames = map fst