+let definition2pres ?recno term2pres d =
+ let name = match d.Content.def_name with Some x -> x|_->assert false in
+ let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
+ let ty = d.Content.def_type in
+ let module P = CicNotationPt in
+ let rec split_pi i t =
+ if i <= 1 then
+ match t with
+ | P.Binder ((`Pi|`Forall),(var,_ as v),t)
+ | P.AttributedTerm (_,P.Binder ((`Pi|`Forall),(var,_ as v),t)) ->
+ [v], var, t
+ | _ -> assert false
+ else
+ match t with
+ | P.Binder ((`Pi|`Forall), var ,ty)
+ | P.AttributedTerm (_, P.Binder ((`Pi|`Forall), var ,ty)) ->
+ let l, r, t = split_pi (i-1) ty in
+ var :: l, r, t
+ | _ -> assert false
+ in
+ let params, rec_param, ty = split_pi rno ty in
+ let body = d.Content.def_term in
+ let params =
+ List.map
+ (function
+ | (name,Some ty) ->
+ B.b_h [] [B.b_text [] "("; term2pres name; B.b_text [] " : ";
+ B.b_space; term2pres ty; B.b_text [] ")"; B.b_space]
+ | (name,None) -> B.b_h [] [term2pres name;B.b_space])
+ params
+ in
+ B.b_hv []
+ [B.b_hov (RenderingAttrs.indent_attributes `BoxML)
+ ( [B.b_hov (RenderingAttrs.indent_attributes `BoxML) ([ B.b_space; B.b_text [] name ] @
+ [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))])]
+ @ [B.b_h []
+ ((if rno <> -1 then
+ [B.b_kw "on";B.b_space;term2pres rec_param] else [])
+ @ [ B.b_space; B.b_text [] ":";]) ]
+ @[ B.indent(term2pres ty)]);
+ B.b_text [] ":=";
+ B.b_h [] [B.b_space;term2pres body] ]
+;;
+
+let joint_def2pres ?recno term2pres def =