From e3ed04fe2299bdb814ee077e60f1046a86156982 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 22 Dec 2006 10:51:43 +0000 Subject: [PATCH] Minor change. --- components/content_pres/content2pres.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/components/content_pres/content2pres.ml b/components/content_pres/content2pres.ml index a15200b16..7c0ad99c4 100644 --- a/components/content_pres/content2pres.ml +++ b/components/content_pres/content2pres.ml @@ -387,7 +387,7 @@ and proof2pres term2pres p = match args with | [] -> [] | (Con.ArgProof p)::(Con.Term t)::tl -> - B.H([],([B.b_kw "=";B.b_space;term2pres t;B.b_space]@justification p))::(aux tl) + B.HOV(RenderingAttrs.indent_attributes `BoxML,([B.b_kw "=";B.b_space;term2pres t;B.b_space]@justification p))::(aux tl) | _ -> assert false in let hd = @@ -395,9 +395,9 @@ and proof2pres term2pres p = | Con.Term t -> t | _ -> assert false in - B.H([],[term2pres hd; B.b_space; + B.HOV([],[term2pres hd; (* B.b_space; *) B.V ([],aux (List.tl conclude.Con.conclude_args))]) - else if conclude.Con.conclude_method = "Apply" then + else if conclude.Con.conclude_method = "Apply" then let pres_args = make_args_for_apply term2pres conclude.Con.conclude_args in B.H([], -- 2.39.2