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