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