make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
in
[B.H([],
- (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::
+ (*(if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::*)
+ (B.b_kw "by")::
B.b_space::
B.Text([],"(")::pres_args@[B.Text([],")")])], None
else
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 -> assert false | Some x -> x 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) -> [v], var, t
+ | 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.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
params
in
B.b_hv []
- [B.b_hv []
- ([ B.b_space; B.b_text [] name ] @ params @
- [B.b_kw "on" ; B.b_space; term2pres rec_param ; B.b_space;
- B.b_text [] ":"; B.b_space; term2pres ty]);
+ [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] ]
;;