let decompose = EliminationTactics.decompose_tac
let discriminate = DiscriminationTactics.discriminate_tac
let elim_intros_simpl = PrimitiveTactics.elim_intros_simpl_tac
+let elim_intros = PrimitiveTactics.elim_intros_tac
let elim_type = EliminationTactics.elim_type_tac
let exact = PrimitiveTactics.exact_tac
let exists = IntroductionTactics.exists_tac
let symmetry = EqualityTactics.symmetry_tac
let transitivity = EqualityTactics.transitivity_tac
let whd = ReductionTactics.whd_tac
-
+let normalize = ReductionTactics.normalize_tac