subtac « plugins - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	equations.ml4	38328	log plain
-rw-r--r--	eterm.ml	7118	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	8413	log plain
-rw-r--r--	subtac.mli	92	log plain
-rw-r--r--	subtac_cases.ml	75963	log plain
-rw-r--r--	subtac_cases.mli	746	log plain
-rw-r--r--	subtac_classes.ml	7252	log plain
-rw-r--r--	subtac_classes.mli	1167	log plain
-rw-r--r--	subtac_coercion.ml	16545	log plain
-rw-r--r--	subtac_coercion.mli	90	log plain
-rw-r--r--	subtac_command.ml	18651	log plain
-rw-r--r--	subtac_command.mli	1516	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	20112	log plain
-rw-r--r--	subtac_obligations.mli	2320	log plain
-rw-r--r--	subtac_plugin.mllib	199	log plain
-rw-r--r--	subtac_pretyping.ml	4730	log plain
-rw-r--r--	subtac_pretyping.mli	670	log plain
-rw-r--r--	subtac_pretyping_F.ml	23315	log plain
-rw-r--r--	subtac_utils.ml	15118	log plain
-rw-r--r--	subtac_utils.mli	4392	log plain
d---------	test	351	log plain