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