@@ -184,24 +184,25 @@ unify' ctxt env topx topy =
184 " in " ++ show env ++
184 " in " ++ show env ++
185 "\nHoles: " ++ show (holes ps) ++ "\n") $
185 "\nHoles: " ++ show (holes ps) ++ "\n") $
186 lift $ unify ctxt env topx topy dont (holes ps)
186 lift $ unify ctxt env topx topy dont (holes ps)
187+ let notu = filter (\ (n, t) -> case t of
189+ _ -> n `elem` dont) u
187 traceWhen (unifylog ps)
190 traceWhen (unifylog ps)
188 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
191 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
189 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
192 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
190 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
193 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
191-- ++ show (pterm ps)
194-- ++ show (pterm ps)
192 ++ "\n----------") $
195 ++ "\n----------") $
196− do ps <- get
196+ do ps <- get
197− let (h, ns) = unified ps
197+ let (h, ns) = unified ps
198− let (ns', probs') = updateProblems (context ps) (u ++ ns)
198+ let (ns', probs') = updateProblems (context ps) (u ++ ns)
199− (err ++ problems ps)
199+ (fails ++ problems ps)
200− (injective ps)
200+ (injective ps)
201− (holes ps)
201+ (holes ps)
202− put (ps { problems = probs',
202+ put (ps { problems = probs',
203− unified = (h, ns') })
203+ unified = (h, ns'),
204+ notunified = notu ++ notunified ps })
204− return u
205+ return u
206getName :: Monad m => String -> StateT TState m Name
207getName :: Monad m => String -> StateT TState m Name
207getName tag = do ps <- get
208getName tag = do ps <- get