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] ]
;;
;;
let content2pres0
- ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
+ ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+ (term2pres : ?prec:int -> 'a)
(id,params,metasenv,obj)
=
match obj with
?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts
=
content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
+(* FG: prec not optional in my patch *)
(fun ?(prec=90) annterm ->
let ast, ids_to_uris =
TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
(TermContentPres.pp_ast ast)))
let ncontent2pres0
- ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
+ ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+ (term2pres : ?prec:int -> 'a)
(id,params,metasenv,obj : CicNotationPt.term Content.cobj)
=
match obj with