let rno = match recno with None -> -1 (* cofix *) | Some x -> x in
let ty = d.Content.def_type in
let module P = NotationPt in
- let rec split_pi i t =
- if i <= 1 then
+ let rec split_pi i t =
+ (* dummy case for corecursive defs *)
+ if i = ~-1 then [], P.UserInput, t
+ else 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)) ->
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))])]
+ if params <> [] then
+ [B.indent(B.b_hov (RenderingAttrs.indent_attributes `BoxML) (params))]
+ else [])]
@ [B.b_h []
((if rno <> -1 then
[B.b_kw "on";B.b_space;term2pres rec_param] else [])
Con.dec_id = dec_id ;
Con.dec_type = ty } = d in
let r =
- Box.b_h [Some "helm", "xref", dec_id]
- [ Box.b_object (p_mi []
- (match dec_name with
- None -> "_"
- | Some n -> n)) ;
- Box.b_space; Box.b_text [] ":"; Box.b_space;
- term2pres ty] in
+ Box.b_hv [Some "helm", "xref", dec_id]
+ [ Box.b_h []
+ [ Box.b_object (p_mi []
+ (match dec_name with
+ None -> "_"
+ | Some n -> n)) ;
+ Box.b_space; Box.b_text [] ":"; ];
+ Box.indent (term2pres ty)] in
aux (r::accum) tl
| (Some (`Definition d))::tl ->
let