added the geniric

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

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 3d189983595ec968e62b30a3724e648d13c729d1..16421efafb386df29236fe77b36e9a9ba05b0cfe 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/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