@@ -739,6 +739,7 @@ keepGiven du (u@(n, _) : us) hs
739 | n `elem` du = u : keepGiven du us hs
739 | n `elem` du = u : keepGiven du us hs
740keepGiven du (u : us) hs = keepGiven du us hs
740keepGiven du (u : us) hs = keepGiven du us hs
742+updateSolved [] x = x
742updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
743updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
743 updateSolved' xs x
744 updateSolved' xs x
744updateSolved' xs (Bind n (Hole ty) t)
745updateSolved' xs (Bind n (Hole ty) t)
@@ -750,9 +751,11 @@ updateSolved' xs (P _ n _)
750 | Just v <- lookup n xs = v
751 | Just v <- lookup n xs = v
751updateSolved' xs t = t
752updateSolved' xs t = t
753updateEnv ns [] = []
755updateEnv ns [] = []
754updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
756updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
758+updateError [] err = err
756updateError ns (CantUnify b l r e xs sc)
759updateError ns (CantUnify b l r e xs sc)
757 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
760 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
758updateError ns e = e
761updateError ns e = e
@@ -762,11 +765,13 @@ solveInProblems x val ((l, r, env, err) : ps)
762 = ((psubst x val l, psubst x val r,
765 = ((psubst x val l, psubst x val r,
763 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
766 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
768+updateNotunified [] nu = nu
765updateNotunified ns nu = up nu where
769updateNotunified ns nu = up nu where
766 up [] = []
770 up [] = []
767 up ((n, t) : ns) = let t' = updateSolved ns t in
771 up ((n, t) : ns) = let t' = updateSolved ns t in
768 ((n, t') : up ns)
772 ((n, t') : up ns)
774+updateProblems ctxt [] ps inj holes = ([], ps)
770updateProblems ctxt ns ps inj holes = up ns ps where
775updateProblems ctxt ns ps inj holes = up ns ps where
771 up ns [] = (ns, [])
776 up ns [] = (ns, [])
772 up ns ((x, y, env, err) : ps) =
777 up ns ((x, y, env, err) : ps) =
@@ -812,7 +817,7 @@ processTactic EndUnify ps
812 (ns'', probs') = updateProblems (context ps) ns' (problems ps)
817 (ns'', probs') = updateProblems (context ps) ns' (problems ps)
813 (injective ps) (holes ps)
818 (injective ps) (holes ps)
814 tm' = -- trace ("Updating " ++ show ns_in ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $
819 tm' = -- trace ("Updating " ++ show ns_in ++ "\n" ++ show ns'') $ -- ++ " in " ++ show (pterm ps)) $
815− updateSolved ns'' (pterm ps) in
820+ updateSolved ns'' (pterm ps) in
816 return (ps { pterm = tm',
821 return (ps { pterm = tm',
817 unified = (h, []),
822 unified = (h, []),
818 problems = probs',
823 problems = probs',