+ | TacticAst.Exists loc -> status, TacticAst.Exists loc
+ | TacticAst.Fold (loc,reduction_kind, term) ->
+ let status, term = disambiguate_term status term in
+ status, TacticAst.Fold (loc,reduction_kind, term)
+ | TacticAst.FwdSimpl (loc, term) ->
+ let status, term = disambiguate_term status term in
+ status, TacticAst.FwdSimpl (loc, term)
+ | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
+ | TacticAst.Generalize (loc,term,ident,pattern) ->
+ let status,term = disambiguate_term status term in
+ let pattern = disambiguate_pattern status.aliases pattern in
+ status, TacticAst.Generalize(loc,term,ident,pattern)
+ | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
+ | TacticAst.Injection (loc,term) ->
+ let status, term = disambiguate_term status term in
+ status, TacticAst.Injection (loc,term)
+ | TacticAst.Intros (loc, num, names) ->
+ status, TacticAst.Intros (loc, num, names)
+ | TacticAst.LApply (loc, to_what, what) ->
+ let status, to_what =
+ match to_what with
+ None -> status,None
+ | Some to_what ->
+ let status, to_what = disambiguate_term status to_what in
+ status, Some to_what
+ in
+ let status, what = disambiguate_term status what in
+ status, TacticAst.LApply (loc, to_what, what)
+ | TacticAst.Left loc -> status, TacticAst.Left loc
+ | TacticAst.LetIn (loc, term, name) ->
+ let status, term = disambiguate_term status term in
+ status, TacticAst.LetIn (loc,term,name)
+ | TacticAst.Reduce (loc, reduction_kind, pattern) ->
+ let pattern = disambiguate_pattern status.aliases pattern in
+ status, TacticAst.Reduce(loc, reduction_kind, pattern)
+ | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc