X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fsequent2pres.ml;h=ad2724134f47562b6c0c58633a3941a26b7a8967;hb=349a0e23813a7f33853e1f8fe48230276ac22934;hp=afd2292ba0bfe7b8823151d2485980ca4a8b3337;hpb=dd8726f655e4fdad063baf456fcfc95f82e079cc;p=helm.git diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml index afd2292ba..ad2724134 100644 --- a/helm/ocaml/cic_transformations/sequent2pres.ml +++ b/helm/ocaml/cic_transformations/sequent2pres.ml @@ -85,11 +85,15 @@ let sequent2pres term2pres (_,_,context,ty) = [] (context2pres context)) in let pres_goal = term2pres ty in - (Box.b_v - [] - [pres_context; - b_ink [None,"width","4cm"; None,"height","1px"]; - pres_goal]) + (Box.b_h [] [ + Box.b_space; + (Box.b_v [] + [Box.b_space; + pres_context; + b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *) + Box.b_space; + pres_goal]) + ]) ;; (*