subtac « contrib - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	FixSub.v	4188	log plain
-rw-r--r--	FunctionalExtensionality.v	1359	log plain
-rw-r--r--	Heq.v	510	log plain
-rw-r--r--	Subtac.v	66	log plain
-rw-r--r--	SubtacTactics.v	4518	log plain
-rw-r--r--	Utils.v	1744	log plain
-rw-r--r--	context.ml	910	log plain
-rw-r--r--	context.mli	233	log plain
-rw-r--r--	eterm.ml	6850	log plain
-rw-r--r--	eterm.mli	1177	log plain
-rw-r--r--	g_eterm.ml4	1297	log plain
-rw-r--r--	g_subtac.ml4	5008	log plain
-rw-r--r--	subtac.ml	6362	log plain
-rw-r--r--	subtac.mli	92	log plain
-rw-r--r--	subtac_cases.ml	84503	log plain
-rw-r--r--	subtac_cases.mli	793	log plain
-rw-r--r--	subtac_coercion.ml	18729	log plain
-rw-r--r--	subtac_coercion.mli	29	log plain
-rw-r--r--	subtac_command.ml	16572	log plain
-rw-r--r--	subtac_command.mli	893	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	13775	log plain
-rw-r--r--	subtac_obligations.mli	1023	log plain
-rw-r--r--	subtac_pretyping.ml	5518	log plain
-rw-r--r--	subtac_pretyping.mli	381	log plain
-rw-r--r--	subtac_pretyping_F.ml	22806	log plain
-rw-r--r--	subtac_utils.ml	20466	log plain
-rw-r--r--	subtac_utils.mli	4023	log plain
d---------	test	351	log plain