X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fsequent2pres.ml;h=ad2724134f47562b6c0c58633a3941a26b7a8967;hb=acf29bdbdcdc6ad8c2d9d27e8a47500981b605cd;hp=57d7d9140a9868d147147cd49774b0ce710732c2;hpb=29969baf115afff7eb9ea9e2ca98d40ab7006dcc;p=helm.git

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index 57d7d9140..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])
+ ])
 ;;
 
 (*
@@ -102,7 +106,6 @@ let sequent2pres ~ids_to_inner_sorts =
 *)
 
 let sequent2pres ~ids_to_inner_sorts =
-prerr_endline "Sequent2pres.sequent2pres";
   sequent2pres
     (fun annterm ->
       let (ast, ids_to_uris) as arg =