let absurd = NegationTactics.absurd_tac
let apply = PrimitiveTactics.apply_tac
+let applyP = PrimitiveTactics.applyP_tac
let applyS = Auto.applyS_tac
let assumption = VariousTactics.assumption_tac
let auto = Auto.auto_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 symmetry = EqualityTactics.symmetry_tac
let transitivity = EqualityTactics.transitivity_tac