@@ -1804,7 +1804,7 @@ elabClass info syn doc fc constraints tn ps ds
1805 getMName (PTy _ _ _ _ _ n _) = nsroot n
1805 getMName (PTy _ _ _ _ _ n _) = nsroot n
1806 tdecl allmeths (PTy doc _ syn _ o n t)
1806 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
1808 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
1808 logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
1809 return ( (n, (toExp (map fst ps) Exp t')),
1809 return ( (n, (toExp (map fst ps) Exp t')),
1810 (n, (doc, o, (toExp (map fst ps) Imp t'))),
1810 (n, (doc, o, (toExp (map fst ps) Imp t'))),
@@ -1902,19 +1902,6 @@ elabClass info syn doc fc constraints tn ps ds
1902 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
1902 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)
1903 toExp ns e sc = sc
1903 toExp ns e sc = sc
1905− -- Abuse of ElabInfo.
1906− -- TODO: Contemplate whether the ElabInfo type should be modified.
1907− minfo :: ElabInfo -> [Name] -> ElabInfo
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,
1915− liftname = id -- Is this appropriate?
1918elabInstance :: ElabInfo -> SyntaxInfo ->
1905elabInstance :: ElabInfo -> SyntaxInfo ->
1919 ElabWhat -> -- phase
1906 ElabWhat -> -- phase
1920 FC -> [PTerm] -> -- constraints
1907 FC -> [PTerm] -> -- constraints