Dn Termdn Btermdn Nbtermdn Tacticals Hipattern Tactics Evar_tactics Hiddentac Elim Dhyp Auto Ind_tables Equality Contradiction Inv Leminv Tacinterp Autorewrite Decl_interp Decl_proof_instr