+ | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
+ | TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width)
+ | TacticAst.Change (loc, what, with_what, pattern) ->
+ let status, cic1 = disambiguate_term status what in
+ let status, cic2 = disambiguate_term status with_what in
+ let pattern = disambiguate_pattern status.aliases pattern in
+ status, TacticAst.Change (loc, cic1, cic2, pattern)
+ | TacticAst.Clear (loc,id) -> status,TacticAst.Clear (loc,id)
+ | TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id)
+ | TacticAst.Compare (loc,term) ->
+ let status, term = disambiguate_term status term in
+ status, TacticAst.Compare (loc,term)
+ | TacticAst.Constructor (loc,n) ->
+ status, TacticAst.Constructor (loc,n)
+ | TacticAst.Contradiction loc ->
+ status, TacticAst.Contradiction loc
+ | TacticAst.Cut (loc, ident, term) ->
+ let status, cic = disambiguate_term status term in
+ status, TacticAst.Cut (loc, ident, cic)
+ | TacticAst.DecideEquality loc ->
+ status, TacticAst.DecideEquality loc
+ | TacticAst.Decompose (loc,term) ->
+ let status,term = disambiguate_term status term in
+ status, TacticAst.Decompose(loc,term)
+ | TacticAst.Discriminate (loc,term) ->
+ let status,term = disambiguate_term status term in
+ status, TacticAst.Discriminate(loc,term)