X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=d52b0e2de830105c80ee5837fe5902e583b2edc4;hb=fa2319814d744d3e374490fe4e4746d9a5c84f1f;hp=912abbcc38d0eadb1dc1235d35010309e719d3e8;hpb=50afaf262195266d156f594cff7e92a6e8898b3e;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 912abbcc3..d52b0e2de 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -182,8 +182,8 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.ApplyS (loc, cic, params)
     | GrafiteAst.Assumption loc ->
         metasenv,GrafiteAst.Assumption loc
-    | GrafiteAst.Auto (loc,params) ->
-        metasenv,GrafiteAst.Auto (loc,params)
+    | GrafiteAst.AutoBatch (loc,params) ->
+        metasenv,GrafiteAst.AutoBatch (loc,params)
     | GrafiteAst.Cases (loc, what, idents) ->
         let metasenv,what = disambiguate_term context metasenv what in
         metasenv,GrafiteAst.Cases (loc, what, idents)
@@ -212,22 +212,22 @@ let rec disambiguate_tactic
     | GrafiteAst.Exact (loc, term) -> 
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Exact (loc, cic)
-    | GrafiteAst.Elim (loc, what, Some using, pattern, depth, idents) ->
+    | GrafiteAst.Elim (loc, what, Some using, pattern, specs) ->
 	let metasenv,what = disambiguate_term context metasenv what in
         let metasenv,using = disambiguate_term context metasenv using in
 	let pattern = disambiguate_pattern pattern in
-        metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, depth, idents)
-    | GrafiteAst.Elim (loc, what, None, pattern, depth, idents) ->
+        metasenv,GrafiteAst.Elim (loc, what, Some using, pattern, specs)
+    | GrafiteAst.Elim (loc, what, None, pattern, specs) ->
 	let metasenv,what = disambiguate_term context metasenv what in
 	let pattern = disambiguate_pattern pattern in
-        metasenv,GrafiteAst.Elim (loc, what, None, pattern, depth, idents)
-    | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
+        metasenv,GrafiteAst.Elim (loc, what, None, pattern, specs)
+    | GrafiteAst.ElimType (loc, what, Some using, specs) ->
         let metasenv,what = disambiguate_term context metasenv what in
         let metasenv,using = disambiguate_term context metasenv using in
-        metasenv,GrafiteAst.ElimType (loc, what, Some using, depth, idents)
-    | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
+        metasenv,GrafiteAst.ElimType (loc, what, Some using, specs)
+    | GrafiteAst.ElimType (loc, what, None, specs) ->
         let metasenv,what = disambiguate_term context metasenv what in
-        metasenv,GrafiteAst.ElimType (loc, what, None, depth, idents)
+        metasenv,GrafiteAst.ElimType (loc, what, None, specs)
     | GrafiteAst.Exists loc ->
         metasenv,GrafiteAst.Exists loc 
     | GrafiteAst.Fail loc ->
@@ -246,8 +246,8 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Generalize (loc,pattern,ident)
     | GrafiteAst.IdTac loc ->
         metasenv,GrafiteAst.IdTac loc
-    | GrafiteAst.Intros (loc, num, names) ->
-        metasenv,GrafiteAst.Intros (loc, num, names)
+    | GrafiteAst.Intros (loc, specs) ->
+        metasenv,GrafiteAst.Intros (loc, specs)
     | GrafiteAst.Inversion (loc, term) ->
        let metasenv,term = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Inversion (loc, term)
@@ -477,6 +477,7 @@ let disambiguate_macro
    | GrafiteAst.Check (loc,term) ->
       let metasenv,term = disambiguate_term context metasenv term in
        metasenv,GrafiteAst.Check (loc,term)
+   | GrafiteAst.AutoInteractive _
    | GrafiteAst.Hint _
    | GrafiteAst.WLocate _
    | GrafiteAst.Inline _ as macro ->