- new tactic subst removes simple non recursive equalities from the context

[helm.git] / helm / software / components / grafite / grafiteAstPp.ml

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 425751b723b0236ccd2834b0153b43706e3837db..e1855014d27e351498d4b138ea95eea84cd9681e 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -152,7 +152,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Right _ -> "right"
   | Ring _ -> "ring"
   | Split _ -> "split"
-  | Subst (_, s) -> "subst " ^ s
+  | Subst _ -> "subst"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
   (* Tattiche Aggiunte *)