let cut = PrimitiveTactics.cut_tac
let decide_equality = DiscriminationTactics.decide_equality_tac
let decompose = EliminationTactics.decompose_tac
-let demodulate = Indexing.demodulate_tac
+let demodulate = Saturation.demodulate_tac
let discriminate = DiscriminationTactics.discriminate_tac
let elim_intros = PrimitiveTactics.elim_intros_tac
let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac