@@ -763,22 +763,6 @@ elab ist info emode opts fn tm
763 = n `elem` ns
763 = n `elem` ns
764 || any (\x -> x `elem` ns) (allTTNames (binderTy b))
764 || any (\x -> x `elem` ns) (allTTNames (binderTy b))
766− -- FIXME: This probably doesn't help us here, but leaving
767− -- it in temporarily... if this comment is still here in master,
768− -- please delete the code!
769− chaseDeps env acc [] = filter (\(n, _) -> n `elem` acc) env
770− chaseDeps env acc ((n,b) : args)
771− = let ns = allTTNames (binderTy b) in
772− extendAcc ns acc args
774− extendAcc [] acc args = chaseDeps env acc args
775− extendAcc (n:ns) acc args
776− | elem n acc = extendAcc ns acc args
777− | otherwise = case lookup n env of
778− Just b -> extendAcc ns (n : acc)
780− Nothing -> extendAcc ns acc args
782 elab' ina fc (PUnifyLog t) = do unifyLog True
766 elab' ina fc (PUnifyLog t) = do unifyLog True
783 elab' ina fc t
767 elab' ina fc t
784 unifyLog False
768 unifyLog False