@@ -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' info syn allmeths n t
1807+ = do t' <- implicit' (minfo info allmeths) 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,6 +1902,19 @@ 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?
1905elabInstance :: ElabInfo -> SyntaxInfo ->
1918elabInstance :: ElabInfo -> SyntaxInfo ->
1906 ElabWhat -> -- phase
1919 ElabWhat -> -- phase
1907 FC -> [PTerm] -> -- constraints
1920 FC -> [PTerm] -> -- constraints