@@ -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' info syn allmeths n t
1807+ = do t' <- implicit' (minfo info allmeths) 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,6 +1902,19 @@ 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+
19051918elabInstance :: ElabInfo -> SyntaxInfo ->
19061919 ElabWhat -> -- phase
19071920 FC -> [PTerm] -> -- constraints