let apply = PrimitiveTactics.apply_tac
let assumption = VariousTactics.assumption_tac
let auto = AutoTactic.auto_tac
-let change = PrimitiveTactics.change_tac
+let change = ReductionTactics.change_tac
let clear = ProofEngineStructuralRules.clear
let clearbody = ProofEngineStructuralRules.clearbody
let compare = DiscriminationTactics.compare_tac
let split = IntroductionTactics.split_tac
let symmetry = EqualityTactics.symmetry_tac
let transitivity = EqualityTactics.transitivity_tac
+let unfold = ReductionTactics.unfold_tac
let whd = ReductionTactics.whd_tac