git.iko.soy/Idris-dev
on master help sign in
Remove debug printouts.
dd502ecMatus Tejiscak
src/Idris/ElabDecls.hs−1
compare with master
unifiedsplit
@@ -207,7 +207,6 @@ elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
207 FC -> FnOpts -> Name -> PTerm -> Idris ()
207 FC -> FnOpts -> Name -> PTerm -> Idris ()
208elabPostulate info syn doc fc opts n ty = do
208elabPostulate info syn doc fc opts n ty = do
209 elabType info syn doc [] fc opts n ty
209 elabType info syn doc [] fc opts n ty
210− logLvl (-10) $ "adding postulate " ++ show n
211 putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState
210 putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState
212 addIBC (IBCPostulate n)
211 addIBC (IBCPostulate n)
213
212
src/Idris/Erasure.hs−1
@@ -92,7 +92,6 @@ performUsageAnalysis = do
92
92
93 -- Check that no postulates are reachable.
93 -- Check that no postulates are reachable.
94 reachablePostulates <- S.intersection reachableNames . idris_postulates <$> getIState
94 reachablePostulates <- S.intersection reachableNames . idris_postulates <$> getIState
95− logLvl (-10) . show . idris_postulates =<< getIState
96 when (not . S.null $ reachablePostulates)
95 when (not . S.null $ reachablePostulates)
97 $ ifail ("reachable postulates: " ++ (show $ S.toList reachablePostulates))
96 $ ifail ("reachable postulates: " ++ (show $ S.toList reachablePostulates))
98
97