let absurd = NegationTactics.absurd_tac
let apply = PrimitiveTactics.apply_tac
-let applyS = AutoTactic.applyS_tac
+let applyS = Auto.applyS_tac
let assumption = VariousTactics.assumption_tac
let auto = AutoTactic.auto_tac
let change = ReductionTactics.change_tac
let contradiction = NegationTactics.contradiction_tac
let cut = PrimitiveTactics.cut_tac
let decompose = EliminationTactics.decompose_tac
-let demodulate = Saturation.demodulate_tac
+let demodulate = Auto.demodulate_tac
let destruct = DiscriminationTactics.destruct_tac
let elim_intros = PrimitiveTactics.elim_intros_tac
let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac