X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=16421efafb386df29236fe77b36e9a9ba05b0cfe;hb=cc3ab906b631ef0edb4402cb622fc3fa96682717;hp=3d189983595ec968e62b30a3724e648d13c729d1;hpb=8f9d476c32c48d14348a61889dc191c7696bd404;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 3d1899835..16421efaf 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -124,10 +124,13 @@ 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) ->
-        metasenv,GrafiteAst.Auto (loc,depth,width,paramodulation,full)
+    | GrafiteAst.Auto (loc,params) ->
+        metasenv,GrafiteAst.Auto (loc,params)
     | GrafiteAst.Change (loc, pattern, with_what) -> 
         let with_what = disambiguate_lazy_term with_what in
         let pattern = disambiguate_pattern pattern in