ltac « plugins - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	coretactics.mlg	10007	log plain
-rw-r--r--	dune	461	log plain
-rw-r--r--	evar_tactics.ml	4474	log plain
-rw-r--r--	evar_tactics.mli	1082	log plain
-rw-r--r--	extraargs.mlg	10726	log plain
-rw-r--r--	extraargs.mli	2785	log plain
-rw-r--r--	extratactics.mlg	36053	log plain
-rw-r--r--	extratactics.mli	962	log plain
-rw-r--r--	g_auto.mlg	8221	log plain
-rw-r--r--	g_class.mlg	4816	log plain
-rw-r--r--	g_eqdecide.mlg	1284	log plain
-rw-r--r--	g_ltac.mlg	18456	log plain
-rw-r--r--	g_obligations.mlg	5952	log plain
-rw-r--r--	g_rewrite.mlg	13764	log plain
-rw-r--r--	g_tactic.mlg	30236	log plain
-rw-r--r--	leminv.ml	10739	log plain
-rw-r--r--	leminv.mli	960	log plain
-rw-r--r--	ltac_plugin.mlpack	293	log plain
-rw-r--r--	pltac.ml	2709	log plain
-rw-r--r--	pltac.mli	2070	log plain
-rw-r--r--	pptactic.ml	55954	log plain
-rw-r--r--	pptactic.mli	6065	log plain
-rw-r--r--	profile_ltac.ml	16343	log plain
-rw-r--r--	profile_ltac.mli	4066	log plain
-rw-r--r--	profile_ltac_tactics.mlg	2849	log plain
-rw-r--r--	rewrite.ml	89989	log plain
-rw-r--r--	rewrite.mli	3977	log plain
-rw-r--r--	tacarg.ml	1880	log plain
-rw-r--r--	tacarg.mli	2565	log plain
-rw-r--r--	taccoerce.ml	15208	log plain
-rw-r--r--	taccoerce.mli	4060	log plain
-rw-r--r--	tacentries.ml	33751	log plain
-rw-r--r--	tacentries.mli	6634	log plain
-rw-r--r--	tacenv.ml	5912	log plain
-rw-r--r--	tacenv.mli	3637	log plain
-rw-r--r--	tacexpr.ml	11070	log plain
-rw-r--r--	tacexpr.mli	11069	log plain
-rw-r--r--	tacintern.ml	33316	log plain
-rw-r--r--	tacintern.mli	2116	log plain
-rw-r--r--	tacinterp.ml	84898	log plain
-rw-r--r--	tacinterp.mli	5395	log plain
-rw-r--r--	tacsubst.ml	12844	log plain
-rw-r--r--	tacsubst.mli	1272	log plain
-rw-r--r--	tactic_debug.ml	15050	log plain
-rw-r--r--	tactic_debug.mli	3274	log plain
-rw-r--r--	tactic_matching.ml	15136	log plain
-rw-r--r--	tactic_matching.mli	2388	log plain
-rw-r--r--	tactic_option.ml	1963	log plain
-rw-r--r--	tactic_option.mli	930	log plain
-rw-r--r--	tauto.ml	9691	log plain
-rw-r--r--	tauto.mli	0	log plain
-rw-r--r--	tauto_plugin.mlpack	6	log plain