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

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

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 151d8cebdb008d4ab83a22159b391f2ee1944d30..cdf01febd9da93bfc81ab797c31283033d696f8c 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -246,8 +246,8 @@ let disambiguate_tactic
         metasenv,GrafiteAst.Ring loc
     | GrafiteAst.Split loc ->
         metasenv,GrafiteAst.Split loc
-    | GrafiteAst.Subst (loc, hyp) ->
-        metasenv, GrafiteAst.Subst (loc, hyp)
+    | GrafiteAst.Subst loc ->
+        metasenv, GrafiteAst.Subst loc
     | GrafiteAst.Symmetry loc ->
         metasenv,GrafiteAst.Symmetry loc
     | GrafiteAst.Transitivity (loc, term) ->