subtac « plugins - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	equations.ml4	37927	log plain
-rw-r--r--	eterm.ml	7056	log plain
-rw-r--r--	eterm.mli	1365	log plain
-rw-r--r--	g_eterm.ml4	1296	log plain
-rw-r--r--	g_subtac.ml4	6054	log plain
-rw-r--r--	subtac.ml	8456	log plain
-rw-r--r--	subtac.mli	92	log plain
-rw-r--r--	subtac_cases.ml	75994	log plain
-rw-r--r--	subtac_cases.mli	746	log plain
-rw-r--r--	subtac_classes.ml	7220	log plain
-rw-r--r--	subtac_classes.mli	1166	log plain
-rw-r--r--	subtac_coercion.ml	16442	log plain
-rw-r--r--	subtac_coercion.mli	90	log plain
-rw-r--r--	subtac_command.ml	18739	log plain
-rw-r--r--	subtac_command.mli	1515	log plain
-rw-r--r--	subtac_errors.ml	650	log plain
-rw-r--r--	subtac_errors.mli	631	log plain
-rw-r--r--	subtac_obligations.ml	20345	log plain
-rw-r--r--	subtac_obligations.mli	2313	log plain
-rw-r--r--	subtac_plugin.mllib	199	log plain
-rw-r--r--	subtac_pretyping.ml	4817	log plain
-rw-r--r--	subtac_pretyping.mli	670	log plain
-rw-r--r--	subtac_pretyping_F.ml	23318	log plain
-rw-r--r--	subtac_utils.ml	15024	log plain
-rw-r--r--	subtac_utils.mli	4389	log plain
d---------	test	351	log plain