]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAstPp.ml
1. rewrite_* and rewrite_back_* merged into one function
[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml
index 33b5e8ade73c04e40d161f74f8fb4c72b66f9dd4..83fdaf0829d7238c20faa991b08f96b373b3201f 100644 (file)
@@ -104,7 +104,8 @@ let rec pp_tactic = function
       sprintf "replace %s with %s" (pp_pattern pattern) (pp_term_ast t)
   | Rewrite (_, pos, t, pattern) -> 
       sprintf "rewrite %s %s %s" 
-        (if pos = `Left then "left" else "right") (pp_term_ast t)
+        (if pos = `LeftToRight then ">" else "<")
+        (pp_term_ast t)
         (pp_pattern pattern)
   | Right _ -> "right"
   | Ring _ -> "ring"