@@ -92,9 +92,8 @@ docFun n
9292 let docstr = case lookupCtxt n (idris_docstrings i) of
9393 [str] -> str
9494 _ -> ""
95− let ty = case lookupTy n (tt_ctxt i) of
96− (t : _) -> t
97− let argnames = map fst (getArgTys ty)
95+ let ty = delabTy i n
96+ let argnames = getPArgNames ty
9897 let args = case lookupCtxt n (idris_implicits i) of
9998 [args] -> zip argnames args
10099 _ -> []
@@ -104,9 +103,11 @@ docFun n
104103 [] -> Nothing
105104 (Fix x _:_) -> Just x
106105
107− return (FD n docstr args (delab i ty) f)
106+ return (FD n docstr args ty f)
108107 where funName :: Name -> String
109108 funName (UN n) = str n
110109 funName (NS n _) = funName n
111110
112−
111+getPArgNames :: PTerm -> [Name]
112+getPArgNames (PPi plicity name ty body) = (name : getPArgNames body)
113+getPArgNames _ = []