added syntax for rewrite (TODO no rewrite-in-Hyp syntax)

[helm.git] / helm / ocaml / cic_transformations / sequent2pres.ml

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index afd2292ba0bfe7b8823151d2485980ca4a8b3337..24a3487b807b3db4fadd2a5f0e0adfc28a7a5064 100644 (file)
--- a/helm/ocaml/cic_transformations/sequent2pres.ml
+++ b/helm/ocaml/cic_transformations/sequent2pres.ml
@@ -85,11 +85,16 @@ 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])
+ ])
 ;;
 
 (*