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

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

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"