@@ -184,24 +184,25 @@ unify' ctxt env topx topy =
184184 " in " ++ show env ++
185185 "\nHoles: " ++ show (holes ps) ++ "\n") $
186186 lift $ unify ctxt env topx topy dont (holes ps)
187+ let notu = filter (\ (n, t) -> case t of
188+ P _ _ _ -> False
189+ _ -> n `elem` dont) u
187190 traceWhen (unifylog ps)
188191 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
189192 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
190193 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
191194-- ++ show (pterm ps)
192195 ++ "\n----------") $
193− case fails of
194−-- [] -> return u
195− err ->
196− do ps <- get
197− let (h, ns) = unified ps
198− let (ns', probs') = updateProblems (context ps) (u ++ ns)
199− (err ++ problems ps)
200− (injective ps)
201− (holes ps)
202− put (ps { problems = probs',
203− unified = (h, ns') })
204− return u
196+ do ps <- get
197+ let (h, ns) = unified ps
198+ let (ns', probs') = updateProblems (context ps) (u ++ ns)
199+ (fails ++ problems ps)
200+ (injective ps)
201+ (holes ps)
202+ put (ps { problems = probs',
203+ unified = (h, ns'),
204+ notunified = notu ++ notunified ps })
205+ return u
205206
206207getName :: Monad m => String -> StateT TState m Name
207208getName tag = do ps <- get