- make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
- B.H([],
- (B.b_kw "by")::B.b_space::
- B.Text([],"(")::pres_args@[B.Text([],")")]), None
- else (B.b_kw "by"),
- Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p])
+ make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
+ in
+ [B.H([],
+ (B.b_kw "by")::B.b_space::
+ B.Text([],"(")::pres_args@[B.Text([],")")])], None
+ else
+ [B.H([],[B.b_kw "by"; B.b_space; B.b_kw "proof"])],
+ Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)])