0ee7bfb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1145 from raichoo/fix1015

Fix #1015

commit0ee7bfbe59450a0efc1f812c552c7f7e44b9458f authorraichoo <raichoo@googlemail.com> dateThu 1 May 2014, 13:35 (12 years ago) parentf9827ac e36c883

2 files changed+2−2

unifiedsplit

src/Idris/Core/Elaborate.hs+1−1

@@ -64,7 +64,7 @@ loadState :: Elab' aux ()

6464loadState = do (ES p s e) <- get

6565 case e of

6666 Just st -> put st

67− _ -> fail "Nothing to undo"

67+ _ -> lift $ Error . Msg $ "Nothing to undo"

6868

6969getNameFrom :: Name -> Elab' aux Name

7070getNameFrom 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

872872 _ -> fail "Still holes to fill."

873873processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

874874processTactic Undo ps = case previous ps of

875− Nothing -> fail "Nothing to undo."

875+ Nothing -> Error . Msg $ "Nothing to undo."

876876 Just pold -> return (pold, "")

877877processTactic EndUnify ps

878878 = let (h, ns_in) = unified ps