@@ -945,7 +945,7 @@ expandParams dec ps ns infs tm = en tm
945 | otherwise = PLam n (en t) (en s)
945 | otherwise = PLam n (en t) (en s)
946 en (PPi p n t s)
946 en (PPi p n t s)
947 | n `elem` (map fst ps ++ ns)
947 | n `elem` (map fst ps ++ ns)
948− = let n' = mkShadow n in -- FIXME THINK SHADOWING TacImp?
948+ = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
949 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
949 PPi (enTacImp p) n' (en t) (en (shadow n n' s))
950 | otherwise = PPi (enTacImp p) n (en t) (en s)
950 | otherwise = PPi (enTacImp p) n (en t) (en s)
951 en (PLet n ty v s)
951 en (PLet n ty v s)