let elim_type2_tac ~term ~proof =
let elim_type2_tac ~term ~proof status =
let module E = EliminationTactics in
warn "in Ring.elim_type2";
ProofEngineTypes.apply_tactic
let elim_type2_tac ~term ~proof =
let elim_type2_tac ~term ~proof status =
let module E = EliminationTactics in
warn "in Ring.elim_type2";
ProofEngineTypes.apply_tactic