From 0e850ea466d664062ad1999e75c60b90aadaa084 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 22 Dec 2006 10:51:43 +0000 Subject: [PATCH] Minor change. --- helm/software/components/content_pres/content2pres.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index a15200b16..7c0ad99c4 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/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