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