@@ -92,9 +92,8 @@ docFun n
92 let docstr = case lookupCtxt n (idris_docstrings i) of
92 let docstr = case lookupCtxt n (idris_docstrings i) of
93 [str] -> str
93 [str] -> str
95− let ty = case lookupTy n (tt_ctxt i) of
95+ let ty = delabTy i n
97− let argnames = map fst (getArgTys ty)
96+ let argnames = getPArgNames ty
98 let args = case lookupCtxt n (idris_implicits i) of
97 let args = case lookupCtxt n (idris_implicits i) of
99 [args] -> zip argnames args
98 [args] -> zip argnames args
@@ -104,9 +103,11 @@ docFun n
104 [] -> Nothing
103 [] -> Nothing
105 (Fix x _:_) -> Just x
104 (Fix x _:_) -> Just x
107− return (FD n docstr args (delab i ty) f)
106+ return (FD n docstr args ty f)
108 where funName :: Name -> String
107 where funName :: Name -> String
109 funName (UN n) = str n
108 funName (UN n) = str n
110 funName (NS n _) = funName n
109 funName (NS n _) = funName n
112−
111+getPArgNames :: PTerm -> [Name]
112+getPArgNames (PPi plicity name ty body) = (name : getPArgNames body)