- metasenv,GrafiteAst.ExistsElim(loc, cic, id1, cic', id2, cic'')
- | GrafiteAst.AndElim (loc, term, id, term1, id1, term2) ->
- let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.ExistsElim(loc, just, id1, cic', id2, cic'')
+ | GrafiteAst.AndElim (loc, just, id, term1, id1, term2) ->
+ let metasenv,just =
+ disambiguate_just disambiguate_term context metasenv just in