Apply-Silvie tactic added!

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

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 3d189983595ec968e62b30a3724e648d13c729d1..0e96aaf2dc871b303ed8436d158ab8a9c3229701 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -124,6 +124,9 @@ let disambiguate_tactic
     | GrafiteAst.Apply (loc, term) ->
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Apply (loc, cic)
+    | GrafiteAst.ApplyS (loc, term) ->
+        let metasenv,cic = disambiguate_term context metasenv term in
+        metasenv,GrafiteAst.ApplyS (loc, cic)
     | GrafiteAst.Assumption loc ->
         metasenv,GrafiteAst.Assumption loc
     | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->