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)
| 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 ->