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

bold sequent line
more space between the sequent line and the formulae

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index e7506a15d7b140adcef126ce8a78d87a5cfd48f2..486c26a7475a5332f9839d838b52a8cff38719e9 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -398,7 +398,10 @@ EXTEND
     | [ IDENT "replace" ];
       t1 = tactic_term; "with"; t2 = tactic_term ->
         TacticAst.Replace (loc, t1, t2)
-    (* TODO Rewrite *)
+    | [ IDENT "rewrite" ; IDENT "left" ] ; t = term ->
+        TacticAst.Rewrite (loc,`Left, t, None)
+    | [ IDENT "rewrite" ; IDENT "right" ] ; t = term ->
+        TacticAst.Rewrite (loc,`Right, t, None)
     (* TODO Replace_pattern *)
     | [ IDENT "right" ] -> TacticAst.Right loc
     | [ IDENT "ring" ] -> TacticAst.Ring loc

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])
+ ])
 ;;
 
 (*

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 99fc38553a49c60b7eeb8b2505511ef9701253c7..f781ea3d763b33a6570989eeee5bb825b79fb0c7 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -87,7 +87,10 @@ let rec pp_tactic = function
   | Replace (_, t1, t2) ->
       sprintf "replace %s with %s" (pp_term_ast t1) (pp_term_ast t2)
   | Replace_pattern (_, _, _) -> assert false  (* TODO *)
-  | Rewrite (_, _, _, _) -> assert false (* TODO *)
+  | Rewrite (_, pos, t, None) -> 
+      sprintf "rewrite %s %s" 
+        (if pos = `Left then "left" else "right") (pp_term_ast t)
+  | Rewrite _ -> assert false (* TODO *)
   | Right _ -> "right"
   | Ring _ -> "ring"
   | Split _ -> "split"