subtac « contrib - debian-coq - Debian packaging for Coq

Mode	Name	Size
-rw-r--r--	FixSub.v	2684	log plain
-rw-r--r--	FunctionalExtensionality.v	788	log plain
-rw-r--r--	Subtac.v	66	log plain
-rw-r--r--	Utils.v	2043	log plain
-rw-r--r--	context.ml	910	log plain
-rw-r--r--	context.mli	233	log plain
-rw-r--r--	eterm.ml	5674	log plain
-rw-r--r--	eterm.mli	1033	log plain
-rw-r--r--	g_eterm.ml4	1345	log plain
-rw-r--r--	g_subtac.ml4	4628	log plain
-rw-r--r--	subtac.ml	8786	log plain
-rw-r--r--	subtac.mli	131	log plain
-rw-r--r--	subtac_cases.ml	73900	log plain
-rw-r--r--	subtac_cases.mli	1669	log plain
-rw-r--r--	subtac_coercion.ml	18291	log plain
-rw-r--r--	subtac_coercion.mli	29	log plain
-rw-r--r--	subtac_command.ml	15121	log plain
-rw-r--r--	subtac_command.mli	892	log plain
-rw-r--r--	subtac_errors.ml	654	log plain
-rw-r--r--	subtac_errors.mli	631	log plain
-rw-r--r--	subtac_interp_fixpoint.ml	4615	log plain
-rw-r--r--	subtac_interp_fixpoint.mli	686	log plain
-rw-r--r--	subtac_obligations.ml	11905	log plain
-rw-r--r--	subtac_obligations.mli	697	log plain
-rw-r--r--	subtac_pretyping.ml	5429	log plain
-rw-r--r--	subtac_pretyping.mli	381	log plain
-rw-r--r--	subtac_pretyping_F.ml	22894	log plain
-rw-r--r--	subtac_utils.ml	22013	log plain
-rw-r--r--	subtac_utils.mli	3886	log plain
d---------	test	317	log plain