- 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([],
+ (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::
+ B.b_space::
+ B.Text([],"(")::pres_args@[B.Text([],")")])], None
+ else
+ [B.H([],
+ if for_rewriting_step then
+ [B.b_kw "proof"]
+ else
+ [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)])