@@ -739,6 +739,7 @@ keepGiven du (u@(n, _) : us) hs
739739 | n `elem` du = u : keepGiven du us hs
740740keepGiven du (u : us) hs = keepGiven du us hs
741741
742+updateSolved [] x = x
742743updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
743744 updateSolved' xs x
744745updateSolved' xs (Bind n (Hole ty) t)
@@ -750,9 +751,11 @@ updateSolved' xs (P _ n _)
750751 | Just v <- lookup n xs = v
751752updateSolved' xs t = t
752753
754+updateEnv [] e = e
753755updateEnv ns [] = []
754756updateEnv ns ((n, b) : env) = (n, fmap (updateSolved ns) b) : updateEnv ns env
755757
758+updateError [] err = err
756759updateError ns (CantUnify b l r e xs sc)
757760 = CantUnify b (updateSolved ns l) (updateSolved ns r) (updateError ns e) xs sc
758761updateError ns e = e
@@ -762,11 +765,13 @@ solveInProblems x val ((l, r, env, err) : ps)
762765 = ((psubst x val l, psubst x val r,
763766 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
764767
768+updateNotunified [] nu = nu
765769updateNotunified ns nu = up nu where
766770 up [] = []
767771 up ((n, t) : ns) = let t' = updateSolved ns t in
768772 ((n, t') : up ns)
769773
774+updateProblems ctxt [] ps inj holes = ([], ps)
770775updateProblems ctxt ns ps inj holes = up ns ps where
771776 up ns [] = (ns, [])
772777 up ns ((x, y, env, err) : ps) =
@@ -812,7 +817,7 @@ processTactic EndUnify ps
812817 (ns'', probs') = updateProblems (context ps) ns' (problems ps)
813818 (injective ps) (holes ps)
814819 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
816821 return (ps { pterm = tm',
817822 unified = (h, []),
818823 problems = probs',