let make_args_for_apply term2pres args =
let module Con = Content in
let module P = Mpresentation in
let make_args_for_apply term2pres args =
let module Con = Content in
let module P = Mpresentation in
- P.smallskip::P.Mi([],"_")::row) in
- match args with
- hd::tl ->
- make_arg_for_apply true hd
- (List.fold_right (make_arg_for_apply false) tl [])
- | _ -> assert false;;
+ P.Mi([],"_")::row
+ in
+ if is_first then res else P.smallskip::res
+ in
+ match args with
+ hd::tl ->
+ make_arg_for_apply true hd
+ (List.fold_right (make_arg_for_apply false) tl [])
+ | _ -> assert false
+;;
make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
P.Mrow([],
P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
P.Mrow([],
P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
P.Mrow ([],
[P.Mtext([None,"mathcolor","Red"],"Suppose");
P.Mspace([None,"width","0.1cm"]);
P.Mrow ([],
[P.Mtext([None,"mathcolor","Red"],"Suppose");
P.Mspace([None,"width","0.1cm"]);
P.Mspace([None,"width","0.1cm"]);
term2pres h.Con.dec_type]))
| _ -> assert false in
P.Mspace([None,"width","0.1cm"]);
term2pres h.Con.dec_type]))
| _ -> assert false in