let apply = PrimitiveTactics.apply_tac
let assumption = VariousTactics.assumption_tac
let auto = AutoTactic.auto_tac
-let auto_new = AutoTactic.auto_tac_new
let change = PrimitiveTactics.change_tac
let compare = DiscriminationTactics.compare_tac
let constructor = IntroductionTactics.constructor_tac