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