X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=cdf01febd9da93bfc81ab797c31283033d696f8c;hb=5412a7f12ed2034b4dfb6104440a2308d6a6e8e1;hp=e4df929d76b6f42e816a174b31fd74aafc965194;hpb=bd277786d78d49594b3ada1c3c9c28cba5dc03b9;p=helm.git

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