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

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 9e9be81e2e675a4165c795ab3ca4ae1be94eaf72..16f7998d19a7ee528d53f46f822b9e0a9d02a3cf 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -233,8 +233,8 @@ EXTEND
         GrafiteAst.Ring loc
     | IDENT "split" ->
         GrafiteAst.Split loc
-    | IDENT "subst"; id = IDENT ->
-        GrafiteAst.Subst (loc, id)    
+    | IDENT "subst" ->
+        GrafiteAst.Subst loc    
     | IDENT "symmetry" ->
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->