tactics - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	.cvsignore	9	log plain
-rw-r--r--	AutoRewrite.v	1505	log plain
-rw-r--r--	EAuto.v	3736	log plain
-rw-r--r--	EqDecide.v	1595	log plain
-rw-r--r--	Equality.v	5012	log plain
-rw-r--r--	Inv.v	4183	log plain
-rw-r--r--	Refine.v	721	log plain
-rw-r--r--	Tauto.v	774	log plain
-rw-r--r--	auto.ml	31412	log plain
-rw-r--r--	auto.mli	4966	log plain
-rw-r--r--	autorewrite.ml	3939	log plain
-rw-r--r--	autorewrite.mli	824	log plain
-rw-r--r--	btermdn.ml	1521	log plain
-rw-r--r--	btermdn.mli	893	log plain
-rw-r--r--	dhyp.ml	9849	log plain
-rw-r--r--	dhyp.mli	685	log plain
-rw-r--r--	dn.ml	2915	log plain
-rw-r--r--	dn.mli	1739	log plain
-rw-r--r--	doc.tex	246	log plain
-rw-r--r--	eauto.ml	11976	log plain
-rw-r--r--	elim.ml	6449	log plain
-rw-r--r--	elim.mli	1480	log plain
-rw-r--r--	eqdecide.ml	6053	log plain
-rw-r--r--	equality.ml	64095	log plain
-rw-r--r--	equality.mli	4242	log plain
-rw-r--r--	hiddentac.ml	1931	log plain
-rw-r--r--	hiddentac.mli	1726	log plain
-rw-r--r--	hipattern.ml	4695	log plain
-rw-r--r--	hipattern.mli	2752	log plain
-rw-r--r--	inv.ml	18777	log plain
-rw-r--r--	inv.mli	1034	log plain
-rw-r--r--	leminv.ml	13068	log plain
-rw-r--r--	nbtermdn.ml	2556	log plain
-rw-r--r--	nbtermdn.mli	1328	log plain
-rw-r--r--	refine.ml	9387	log plain
-rw-r--r--	refine.mli	651	log plain
-rw-r--r--	tacentries.ml	2803	log plain
-rw-r--r--	tacentries.mli	2195	log plain
-rw-r--r--	tacticals.ml	14911	log plain
-rw-r--r--	tacticals.mli	5572	log plain
-rw-r--r--	tactics.ml	59754	log plain
-rw-r--r--	tactics.mli	9078	log plain
-rw-r--r--	tauto.ml4	4539	log plain
-rw-r--r--	termdn.ml	2342	log plain
-rw-r--r--	termdn.mli	1621	log plain
-rw-r--r--	wcclausenv.ml	6881	log plain
-rw-r--r--	wcclausenv.mli	1952	log plain