let cut = PrimitiveTactics.cut_tac
let decompose = EliminationTactics.decompose_tac
let demodulate = Auto.demodulate_tac
-let destruct = DiscriminationTactics.destruct_tac
+let destruct = DestructTactic.destruct_tac
let elim_intros = PrimitiveTactics.elim_intros_tac
let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac
let elim_type = EliminationTactics.elim_type_tac
let right = IntroductionTactics.right_tac
let ring = Ring.ring_tac
let simpl = ReductionTactics.simpl_tac
+let solve_rewrite = Auto.solve_rewrite_tac
let split = IntroductionTactics.split_tac
-let subst = SubstTactic.subst_tac
let symmetry = EqualityTactics.symmetry_tac
let transitivity = EqualityTactics.transitivity_tac
let unfold = ReductionTactics.unfold_tac