- | TacticAst.Elim (loc, term, Some term') ->
- let status, cic1 = disambiguate_term status term in
- let status, cic2 = disambiguate_term status term' in
- status, TacticAst.Elim (loc, cic1, Some cic2)
- | TacticAst.Elim (loc, term, None) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Elim (loc, cic, None)
- | TacticAst.ElimType (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.ElimType (loc, cic)
+ | TacticAst.Elim (loc, what, Some using, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ let status, using = disambiguate_term status using in
+ status, TacticAst.Elim (loc, what, Some using, depth, idents)
+ | TacticAst.Elim (loc, what, None, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ status, TacticAst.Elim (loc, what, None, depth, idents)
+ | TacticAst.ElimType (loc, what, Some using, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ let status, using = disambiguate_term status using in
+ status, TacticAst.ElimType (loc, what, Some using, depth, idents)
+ | TacticAst.ElimType (loc, what, None, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ status, TacticAst.ElimType (loc, what, None, depth, idents)