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

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

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