subtac « contrib - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	equations.ml4	38328	log plain
-rw-r--r--	eterm.ml	7280	log plain
-rw-r--r--	eterm.mli	1370	log plain
-rw-r--r--	g_eterm.ml4	1297	log plain
-rw-r--r--	g_subtac.ml4	5891	log plain
-rw-r--r--	subtac.ml	8461	log plain
-rw-r--r--	subtac.mli	92	log plain
-rw-r--r--	subtac_cases.ml	79942	log plain
-rw-r--r--	subtac_cases.mli	746	log plain
-rw-r--r--	subtac_classes.ml	7248	log plain
-rw-r--r--	subtac_classes.mli	1167	log plain
-rw-r--r--	subtac_coercion.ml	16579	log plain
-rw-r--r--	subtac_coercion.mli	90	log plain
-rw-r--r--	subtac_command.ml	17356	log plain
-rw-r--r--	subtac_command.mli	1105	log plain
-rw-r--r--	subtac_errors.ml	654	log plain
-rw-r--r--	subtac_errors.mli	631	log plain
-rw-r--r--	subtac_obligations.ml	20029	log plain
-rw-r--r--	subtac_obligations.mli	2310	log plain
-rw-r--r--	subtac_plugin.mllib	181	log plain
-rw-r--r--	subtac_pretyping.ml	4724	log plain
-rw-r--r--	subtac_pretyping.mli	642	log plain
-rw-r--r--	subtac_pretyping_F.ml	23531	log plain
-rw-r--r--	subtac_utils.ml	14963	log plain
-rw-r--r--	subtac_utils.mli	4368	log plain
d---------	test	351	log plain