X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=ececcf967934f82ee5ccbbeb150b07b85e405b15;hb=c2a02fcbcaaef7358acebcb27014db4a601ad026;hp=912abbcc38d0eadb1dc1235d35010309e719d3e8;hpb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;p=helm.git

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 912abbcc3..ececcf967 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/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)
@@ -195,6 +195,16 @@ let rec disambiguate_tactic
         metasenv,GrafiteAst.Clear (loc,id)
     | GrafiteAst.ClearBody (loc,id) ->
        metasenv,GrafiteAst.ClearBody (loc,id)
+    | GrafiteAst.Compose (loc, t1, t2, times, spec) ->
+        let metasenv,t1 = disambiguate_term context metasenv t1 in
+        let metasenv,t2 = 
+          match t2 with
+          | None -> metasenv, None
+          | Some t2 -> 
+              let m, t2 = disambiguate_term context metasenv t2 in
+              m, Some t2
+        in
+        metasenv,   GrafiteAst.Compose (loc, t1, t2, times, spec)
     | GrafiteAst.Constructor (loc,n) ->
         metasenv,GrafiteAst.Constructor (loc,n)
     | GrafiteAst.Contradiction loc ->
@@ -212,22 +222,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 +256,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 +487,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 ->