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)
metasenv,GrafiteAst.Clear (loc,id)
| GrafiteAst.ClearBody (loc,id) ->
metasenv,GrafiteAst.ClearBody (loc,id)
+ | GrafiteAst.Compose (loc, t1, t2, spec) ->
+ let metasenv,t1 = disambiguate_term context metasenv t1 in
+ let metasenv,t2 = disambiguate_term context metasenv t2 in
+ metasenv, GrafiteAst.Compose (loc, t1, t2, spec)
| GrafiteAst.Constructor (loc,n) ->
metasenv,GrafiteAst.Constructor (loc,n)
| GrafiteAst.Contradiction loc ->
| 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 ->