Dn Termdn Btermdn Nbtermdn Tacticals Hipattern Ind_tables Eqschemes Elimschemes Tactics Hiddentac Elim Dhyp Auto Equality Contradiction Inv Leminv Tacinterp Evar_tactics Autorewrite Tactic_option