X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=16421efafb386df29236fe77b36e9a9ba05b0cfe;hb=3b7bfb05e6fc1a2ac6864d8f7d959fcda0597d21;hp=0e96aaf2dc871b303ed8436d158ab8a9c3229701;hpb=ac8bbbb47941fdf5b2d602b1e2ab2a6d6dcec9cd;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 0e96aaf2d..16421efaf 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -129,8 +129,8 @@ let disambiguate_tactic
         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