let cut = PrimitiveTactics.cut_tac
let decompose = EliminationTactics.decompose_tac
let demodulate = Saturation.demodulate_tac
-let discriminate = DiscriminationTactics.discriminate_tac
+let destruct = DiscriminationTactics.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 fwd_simpl = FwdSimplTactic.fwd_simpl_tac
let generalize = VariousTactics.generalize_tac
let id = Tacticals.id_tac
-let injection = DiscriminationTactics.injection_tac
let intros = PrimitiveTactics.intros_tac
let inversion = Inversion.inversion_tac
let lapply = FwdSimplTactic.lapply_tac