| GrafiteAst.Destruct (loc, None) ->
metasenv,GrafiteAst.Destruct(loc,None)
| 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, specs) ->
| GrafiteAst.Destruct (loc, None) ->
metasenv,GrafiteAst.Destruct(loc,None)
| 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, specs) ->