ltac « plugins - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Ltac.v	0	log plain
-rw-r--r--	coretactics.ml4	10220	log plain
-rw-r--r--	evar_tactics.ml	4009	log plain
-rw-r--r--	evar_tactics.mli	932	log plain
-rw-r--r--	extraargs.ml4	13349	log plain
-rw-r--r--	extraargs.mli	2688	log plain
-rw-r--r--	extratactics.ml4	38450	log plain
-rw-r--r--	extratactics.mli	811	log plain
-rw-r--r--	g_auto.ml4	6892	log plain
-rw-r--r--	g_class.ml4	3863	log plain
-rw-r--r--	g_eqdecide.ml4	1159	log plain
-rw-r--r--	g_ltac.ml4	19469	log plain
-rw-r--r--	g_obligations.ml4	5628	log plain
-rw-r--r--	g_rewrite.ml4	12710	log plain
-rw-r--r--	g_tactic.ml4	27842	log plain
-rw-r--r--	ltac_plugin.mlpack	278	log plain
-rw-r--r--	pltac.ml	2531	log plain
-rw-r--r--	pltac.mli	1775	log plain
-rw-r--r--	pptactic.ml	47625	log plain
-rw-r--r--	pptactic.mli	3836	log plain
-rw-r--r--	profile_ltac.ml	14434	log plain
-rw-r--r--	profile_ltac.mli	1861	log plain
-rw-r--r--	profile_ltac_tactics.ml4	1474	log plain
-rw-r--r--	rewrite.ml	84031	log plain
-rw-r--r--	rewrite.mli	3530	log plain
-rw-r--r--	tacarg.ml	929	log plain
-rw-r--r--	tacarg.mli	1177	log plain
-rw-r--r--	taccoerce.ml	11594	log plain
-rw-r--r--	taccoerce.mli	3301	log plain
-rw-r--r--	tacentries.ml	18001	log plain
-rw-r--r--	tacentries.mli	2778	log plain
-rw-r--r--	tacenv.ml	4297	log plain
-rw-r--r--	tacenv.mli	2772	log plain
-rw-r--r--	tacexpr.mli	11824	log plain
-rw-r--r--	tacintern.ml	31377	log plain
-rw-r--r--	tacintern.mli	2059	log plain
-rw-r--r--	tacinterp.ml	82304	log plain
-rw-r--r--	tacinterp.mli	5133	log plain
-rw-r--r--	tacsubst.ml	12560	log plain
-rw-r--r--	tacsubst.mli	1108	log plain
-rw-r--r--	tactic_debug.ml	14886	log plain
-rw-r--r--	tactic_debug.mli	3156	log plain
-rw-r--r--	tactic_matching.ml	15060	log plain
-rw-r--r--	tactic_matching.mli	2218	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	9829	log plain
-rw-r--r--	tauto.mli	0	log plain
-rw-r--r--	tauto_plugin.mlpack	6	log plain