+ let metasenv,cic' = disambiguate_term context metasenv term' in
+ metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic')
+ | GrafiteAst.Byinduction (loc, term, id) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Byinduction(loc, cic, id)
+ | GrafiteAst.Thesisbecomes (loc, term) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,GrafiteAst.Thesisbecomes (loc, cic)
+ | GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) ->
+ let metasenv,cic =
+ match term with
+ None -> metasenv,None
+ | Some t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some t in
+ let metasenv,cic' = disambiguate_term context metasenv term1 in
+ let cic''= disambiguate_lazy_term term2 in
+ 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
+ let metasenv,cic'= disambiguate_term context metasenv term1 in
+ let metasenv,cic''= disambiguate_term context metasenv term2 in
+ metasenv,GrafiteAst.AndElim(loc, cic, id, cic', id1, cic'')
+ | GrafiteAst.Case (loc, id, params) ->
+ let metasenv,params' =
+ List.fold_right
+ (fun (id,term) (metasenv,params) ->
+ let metasenv,cic = disambiguate_term context metasenv term in
+ metasenv,(id,cic)::params
+ ) params (metasenv,[])
+ in
+ metasenv,GrafiteAst.Case(loc, id, params')
+ | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
+ let metasenv,cic =
+ match term1 with
+ None -> metasenv,None
+ | Some (start,t) ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,Some (start,t) in
+ let metasenv,cic'= disambiguate_term context metasenv term2 in
+ let metasenv,cic'' =
+ match term3 with
+ `Auto _ as t -> metasenv,t
+ | `Term t ->
+ let metasenv,t = disambiguate_term context metasenv t in
+ metasenv,`Term t
+ | `Proof as t -> metasenv,t in
+ metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)
+