- status, TacticAst.ElimType (loc, cic)
- | TacticAst.Replace (loc, what, with_what) ->
- let status, cic1 = disambiguate_term status what in
- let status, cic2 = disambiguate_term status with_what in
- status, TacticAst.Replace (loc, cic1, cic2)
- | TacticAst.Change (loc, what, with_what, ident) ->
- let status, cic1 = disambiguate_term status what in
- let status, cic2 = disambiguate_term status with_what in
- status, TacticAst.Change (loc, cic1, cic2, ident)
-(*
- (* TODO Zack a lot more of tactics to be implemented here ... *)
- | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
- | TacticAst.Change of 'term * 'term * 'ident option
- | TacticAst.Decompose of 'ident * 'ident list
- | TacticAst.Discriminate of 'ident
- | TacticAst.Fold of reduction_kind * 'term
- | TacticAst.Injection of 'ident
- | TacticAst.LetIn of 'term * 'ident
- | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
- | TacticAst.Replace_pattern of 'term pattern * 'term
-*)
- | TacticAst.Rewrite (loc,dir,t,ident) ->
+ status, GrafiteAst.Exact (loc, cic)
+ | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ let status, using = disambiguate_term status using in
+ status, GrafiteAst.Elim (loc, what, Some using, depth, idents)
+ | GrafiteAst.Elim (loc, what, None, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ status, GrafiteAst.Elim (loc, what, None, depth, idents)
+ | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ let status, using = disambiguate_term status using in
+ status, GrafiteAst.ElimType (loc, what, Some using, depth, idents)
+ | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ status, GrafiteAst.ElimType (loc, what, None, depth, idents)
+ | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc
+ | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc
+ | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
+ let status, pattern = disambiguate_pattern status pattern in
+ let status, term = disambiguate_term status term in
+ let status, red_kind = disambiguate_reduction_kind status red_kind in
+ status, GrafiteAst.Fold (loc,red_kind, term, pattern)
+ | GrafiteAst.FwdSimpl (loc, hyp, names) ->
+ status, GrafiteAst.FwdSimpl (loc, hyp, names)
+ | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc
+ | GrafiteAst.Generalize (loc,pattern,ident) ->
+ let status, pattern = disambiguate_pattern status pattern in
+ status, GrafiteAst.Generalize(loc,pattern,ident)
+ | GrafiteAst.Goal (loc, g) -> status, GrafiteAst.Goal (loc, g)
+ | GrafiteAst.IdTac loc -> status,GrafiteAst.IdTac loc
+ | GrafiteAst.Injection (loc,term) ->
+ let status, term = disambiguate_term status term in
+ status, GrafiteAst.Injection (loc,term)
+ | GrafiteAst.Intros (loc, num, names) ->
+ status, GrafiteAst.Intros (loc, num, names)
+ | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
+ let f term (status, to_what) =
+ let status, term = disambiguate_term status term in
+ status, term :: to_what
+ in
+ let status, to_what = List.fold_right f to_what (status, []) in
+ let status, what = disambiguate_term status what in
+ status, GrafiteAst.LApply (loc, depth, to_what, what, ident)
+ | GrafiteAst.Left loc -> status, GrafiteAst.Left loc
+ | GrafiteAst.LetIn (loc, term, name) ->
+ let status, term = disambiguate_term status term in
+ status, GrafiteAst.LetIn (loc,term,name)
+ | GrafiteAst.Reduce (loc, red_kind, pattern) ->
+ let status, pattern = disambiguate_pattern status pattern in
+ let status, red_kind = disambiguate_reduction_kind status red_kind in
+ status, GrafiteAst.Reduce(loc, red_kind, pattern)
+ | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc
+ | GrafiteAst.Replace (loc, pattern, with_what) ->
+ let status, pattern = disambiguate_pattern status pattern in
+ let status, with_what = disambiguate_term status with_what in
+ status, GrafiteAst.Replace (loc, pattern, with_what)
+ | GrafiteAst.Rewrite (loc, dir, t, pattern) ->