ltac - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	coretactics.ml4	9139	log plain
-rw-r--r--	evar_tactics.ml	3201	log plain
-rw-r--r--	evar_tactics.mli	883	log plain
-rw-r--r--	extraargs.ml4	12306	log plain
-rw-r--r--	extraargs.mli	2411	log plain
-rw-r--r--	extratactics.ml4	36582	log plain
-rw-r--r--	extratactics.mli	810	log plain
-rw-r--r--	g_auto.ml4	6337	log plain
-rw-r--r--	g_class.ml4	3581	log plain
-rw-r--r--	g_eqdecide.ml4	1158	log plain
-rw-r--r--	g_ltac.ml4	19064	log plain
-rw-r--r--	g_obligations.ml4	5638	log plain
-rw-r--r--	g_rewrite.ml4	12278	log plain
-rw-r--r--	g_tactic.ml4	25115	log plain
-rw-r--r--	ltac.mllib	284	log plain
-rw-r--r--	pltac.ml	2474	log plain
-rw-r--r--	pltac.mli	1690	log plain
-rw-r--r--	pptactic.ml	50036	log plain
-rw-r--r--	pptactic.mli	2191	log plain
-rw-r--r--	pptacticsig.mli	2682	log plain
-rw-r--r--	profile_ltac.ml	14331	log plain
-rw-r--r--	profile_ltac.mli	1806	log plain
-rw-r--r--	profile_ltac_tactics.ml4	1349	log plain
-rw-r--r--	rewrite.ml	82429	log plain
-rw-r--r--	rewrite.mli	3427	log plain
-rw-r--r--	tacarg.ml	929	log plain
-rw-r--r--	tacarg.mli	1177	log plain
-rw-r--r--	taccoerce.ml	11341	log plain
-rw-r--r--	taccoerce.mli	3125	log plain
-rw-r--r--	tacentries.ml	17874	log plain
-rw-r--r--	tacentries.mli	2735	log plain
-rw-r--r--	tacenv.ml	4286	log plain
-rw-r--r--	tacenv.mli	2784	log plain
-rw-r--r--	tacexpr.mli	11819	log plain
-rw-r--r--	tacintern.ml	31241	log plain
-rw-r--r--	tacintern.mli	2012	log plain
-rw-r--r--	tacinterp.ml	83081	log plain
-rw-r--r--	tacinterp.mli	4406	log plain
-rw-r--r--	tacsubst.ml	12499	log plain
-rw-r--r--	tacsubst.mli	1108	log plain
-rw-r--r--	tactic_debug.ml	14470	log plain
-rw-r--r--	tactic_debug.mli	3108	log plain
-rw-r--r--	tactic_matching.ml	15048	log plain
-rw-r--r--	tactic_matching.mli	2199	log plain
-rw-r--r--	tactic_option.ml	1962	log plain
-rw-r--r--	tactic_option.mli	790	log plain
-rw-r--r--	tauto.ml	9513	log plain
-rw-r--r--	tauto.mli	0	log plain