git.iko.soy/Idris-dev
on master help sign in
Don't give INTERNAL ERROR when abandoning a proof
d95808eEdwin Brady
src/Idris/Prover.hs+2−2
compare with master
unifiedsplit
@@ -179,10 +179,10 @@ ploop d prompt prf e h
179 i <- receiveInput e
179 i <- receiveInput e
180 return (i, h)
180 return (i, h)
181 (cmd, step) <- case x of
181 (cmd, step) <- case x of
182− Nothing -> do iPrintError ""; fail "Abandoned"
182+ Nothing -> do iPrintError ""; ifail "Abandoned"
183 Just input -> do return (parseTactic i input, input)
183 Just input -> do return (parseTactic i input, input)
184 case cmd of
184 case cmd of
185− Success Abandon -> do iPrintError ""; fail "Abandoned"
185+ Success Abandon -> do iPrintError ""; ifail "Abandoned"
186 _ -> return ()
186 _ -> return ()
187 (d, st, done, prf') <- idrisCatch
187 (d, st, done, prf') <- idrisCatch
188 (case cmd of
188 (case cmd of