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