git.iko.soy/Idris-dev
on master help sign in
Remove dead code
cbbdb3eDavid Raymond Christiansen
src/Idris/Core/Elaborate.hs−7
compare with master
unifiedsplit
@@ -28,13 +28,6 @@ import Debug.Trace
28
28
29import Util.Pretty hiding (fill)
29import Util.Pretty hiding (fill)
30
30
31−-- I don't really want this here, but it's useful for the test shell
32−data Command = Theorem Name Raw
33− | Eval Raw
34− | Quit
35− | Print Name
36− | Tac (Elab ())
37−
38data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
31data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
39 deriving Show
32 deriving Show
40
33