@@ -1804,7 +1804,7 @@ elabClass info syn doc fc constraints tn ps ds
18041804
18051805 getMName (PTy _ _ _ _ _ n _) = nsroot n
18061806 tdecl allmeths (PTy doc _ syn _ o n t)
1807− = do t' <- implicit' (minfo info allmeths) syn allmeths n t
1807+ = do t' <- implicit' info syn allmeths n t
18081808 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
18091809 return ( (n, (toExp (map fst ps) Exp t')),
18101810 (n, (doc, o, (toExp (map fst ps) Imp t'))),
@@ -1902,19 +1902,6 @@ elabClass info syn doc fc constraints tn ps ds
19021902 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
19031903 toExp ns e sc = sc
19041904
1905− -- Abuse of ElabInfo.
1906− -- TODO: Contemplate whether the ElabInfo type should be modified.
1907− minfo :: ElabInfo -> [Name] -> ElabInfo
1908− minfo info ds
1909− = let newps = params info
1910− dsParams = map (\n -> (n, [])) ds
1911− newb = addAlist dsParams (inblock info)
1912− l = liftname info in
1913− info { params = newps,
1914− inblock = newb,
1915− liftname = id -- Is this appropriate?
1916− }
1917−
19181905elabInstance :: ElabInfo -> SyntaxInfo ->
19191906 ElabWhat -> -- phase
19201907 FC -> [PTerm] -> -- constraints