git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1145 from raichoo/fix1015
0ee7bfbraichoo
src/Idris/Core/Elaborate.hs+1−1
compare with master
unifiedsplit
@@ -64,7 +64,7 @@ loadState :: Elab' aux ()
64loadState = do (ES p s e) <- get
64loadState = do (ES p s e) <- get
65 case e of
65 case e of
66 Just st -> put st
66 Just st -> put st
67− _ -> fail "Nothing to undo"
67+ _ -> lift $ Error . Msg $ "Nothing to undo"
68
68
69getNameFrom :: Name -> Elab' aux Name
69getNameFrom :: Name -> Elab' aux Name
70getNameFrom n = do (ES (p, a) s e) <- get
70getNameFrom n = do (ES (p, a) s e) <- get
src/Idris/Core/ProofState.hs+1−1
@@ -872,7 +872,7 @@ processTactic QED ps = case holes ps of
872 _ -> fail "Still holes to fill."
872 _ -> fail "Still holes to fill."
873processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
873processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
874processTactic Undo ps = case previous ps of
874processTactic Undo ps = case previous ps of
875− Nothing -> fail "Nothing to undo."
875+ Nothing -> Error . Msg $ "Nothing to undo."
876 Just pold -> return (pold, "")
876 Just pold -> return (pold, "")
877processTactic EndUnify ps
877processTactic EndUnify ps
878 = let (h, ns_in) = unified ps
878 = let (h, ns_in) = unified ps