git.iko.soy/Idris-dev
on master help sign in
Remove debug printouts.
commitdd502ecf3e94e0b97afa405cba7cc5c4df2504fc authorMatus Tejiscak <ziman@functor.sk> dateThu 27 Mar 2014, 17:12 (13 years ago) parenta88053b
2 files changed−2
compare with master
unifiedsplit
src/Idris/ElabDecls.hs−1 src/Idris/Erasure.hs−1
src/Idris/ElabDecls.hs−1
@@ -207,7 +207,6 @@ elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring ->
207207 FC -> FnOpts -> Name -> PTerm -> Idris ()
208208elabPostulate info syn doc fc opts n ty = do
209209 elabType info syn doc [] fc opts n ty
210− logLvl (-10) $ "adding postulate " ++ show n
211210 putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState
212211 addIBC (IBCPostulate n)
213212
src/Idris/Erasure.hs−1
@@ -92,7 +92,6 @@ performUsageAnalysis = do
9292
9393 -- Check that no postulates are reachable.
9494 reachablePostulates <- S.intersection reachableNames . idris_postulates <$> getIState
95− logLvl (-10) . show . idris_postulates =<< getIState
9695 when (not . S.null $ reachablePostulates)
9796 $ ifail ("reachable postulates: " ++ (show $ S.toList reachablePostulates))
9897