metasenv,GrafiteAst.Assumption loc
| GrafiteAst.Auto (loc,params) ->
metasenv,GrafiteAst.Auto (loc,params)
+ | GrafiteAst.Cases (loc, what, idents) ->
+ let metasenv,what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.Cases (loc, what, idents)
| GrafiteAst.Change (loc, pattern, with_what) ->
let with_what = disambiguate_lazy_term with_what in
let pattern = disambiguate_pattern pattern in
metasenv,GrafiteAst.Reduce(loc, red_kind, pattern)
| GrafiteAst.Reflexivity loc ->
metasenv,GrafiteAst.Reflexivity loc
+ | GrafiteAst.Rename (loc, froms, tos) ->
+ metasenv,GrafiteAst.Rename (loc, froms, tos)
| GrafiteAst.Replace (loc, pattern, with_what) ->
let pattern = disambiguate_pattern pattern in
let with_what = disambiguate_lazy_term with_what in
metasenv,GrafiteAst.Replace (loc, pattern, with_what)
- | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
+ | GrafiteAst.Rewrite (loc, dir, t, pattern, names) ->
let metasenv,term = disambiguate_term context metasenv t in
let pattern = disambiguate_pattern pattern in
- metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern)
+ metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern, names)
| GrafiteAst.Right loc ->
metasenv,GrafiteAst.Right loc
| GrafiteAst.Ring loc ->
let metasenv,t = disambiguate_term context metasenv t in
metasenv,Some t in
metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,cic'')
+ | GrafiteAst.We_proceed_by_cases_on (loc, term, term') ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ let metasenv,cic' = disambiguate_term context metasenv term' in
+ metasenv,GrafiteAst.We_proceed_by_cases_on (loc, cic, cic')
| GrafiteAst.We_proceed_by_induction_on (loc, term, term') ->
let metasenv,cic = disambiguate_term context metasenv term in
let metasenv,cic' = disambiguate_term context metasenv term' in