@@ -212,10 +212,11 @@ unify' ctxt env topx topy =
212212 (fails ++ problems ps)
213213 (injective ps)
214214 (holes ps)
215− put (ps { problems = probs',
215+ let (notu', probs_notu) = mergeNotunified env (notu ++ notunified ps)
216+ put (ps { problems = probs' ++ probs_notu,
216217 unified = (h, ns'),
217218 injective = updateInj u (injective ps),
218− notunified = notu ++ notunified ps })
219+ notunified = notu' })
219220 return u
220221 where updateInj ((n, a) : us) inj
221222 | (P _ n' _, _) <- unApply a,
@@ -812,6 +813,14 @@ solveInProblems x val ((l, r, env, err) : ps)
812813 = ((psubst x val l, psubst x val r,
813814 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
814815
816+mergeNotunified :: Env -> [(Name, Term)] -> ([(Name, Term)], Fails)
817+mergeNotunified env ns = mnu ns [] [] where
818+ mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
819+ mnu ((n, t):ns) ns_acc ps_acc
820+ | Just t' <- lookup n ns = mnu ns ((n,t) : ns_acc)
821+ ((t,t',env,Msg "", [],Match) : ps_acc)
822+ | otherwise = mnu ns ((n,t) : ns_acc) ps_acc
823+
815824updateNotunified [] nu = nu
816825updateNotunified ns nu = up nu where
817826 up [] = []
@@ -877,8 +886,7 @@ processTactic EndUnify ps
877886 notunified = updateNotunified ns'' (notunified ps),
878887 holes = holes ps \\ map fst ns'' }, "")
879888processTactic UnifyAll ps
880− = trace (show (notunified ps)) $
881− let tm' = updateSolved (notunified ps) (pterm ps) in
889+ = let tm' = updateSolved (notunified ps) (pterm ps) in
882890 return (ps { pterm = tm',
883891 notunified = [],
884892 holes = holes ps \\ map fst (notunified ps) }, "")