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

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

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index efcd210713db9c3f2bafa06733f47d3108975883..54924ff4c87351c3cd04f4eb1a963841fbdd4f5b 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -83,7 +83,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Right of loc
   | Ring of loc
   | Split of loc
-  | Subst of loc * string
+  | Subst of loc
   | Symmetry of loc
   | Transitivity of loc * 'term
   (* Costruttori Aggiunti *)