ltac « plugins - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Ltac.v	0	log plain
-rw-r--r--	coretactics.ml4	10229	log plain
-rw-r--r--	evar_tactics.ml	4018	log plain
-rw-r--r--	evar_tactics.mli	941	log plain
-rw-r--r--	extraargs.ml4	13358	log plain
-rw-r--r--	extraargs.mli	2697	log plain
-rw-r--r--	extratactics.ml4	38459	log plain
-rw-r--r--	extratactics.mli	820	log plain
-rw-r--r--	g_auto.ml4	6901	log plain
-rw-r--r--	g_class.ml4	3872	log plain
-rw-r--r--	g_eqdecide.ml4	1168	log plain
-rw-r--r--	g_ltac.ml4	19478	log plain
-rw-r--r--	g_obligations.ml4	5637	log plain
-rw-r--r--	g_rewrite.ml4	12719	log plain
-rw-r--r--	g_tactic.ml4	27851	log plain
-rw-r--r--	ltac_plugin.mlpack	278	log plain
-rw-r--r--	pltac.ml	2540	log plain
-rw-r--r--	pltac.mli	1784	log plain
-rw-r--r--	pptactic.ml	47634	log plain
-rw-r--r--	pptactic.mli	3845	log plain
-rw-r--r--	profile_ltac.ml	14443	log plain
-rw-r--r--	profile_ltac.mli	1870	log plain
-rw-r--r--	profile_ltac_tactics.ml4	1483	log plain
-rw-r--r--	rewrite.ml	84040	log plain
-rw-r--r--	rewrite.mli	3539	log plain
-rw-r--r--	tacarg.ml	938	log plain
-rw-r--r--	tacarg.mli	1186	log plain
-rw-r--r--	taccoerce.ml	11603	log plain
-rw-r--r--	taccoerce.mli	3310	log plain
-rw-r--r--	tacentries.ml	18010	log plain
-rw-r--r--	tacentries.mli	2787	log plain
-rw-r--r--	tacenv.ml	4306	log plain
-rw-r--r--	tacenv.mli	2781	log plain
-rw-r--r--	tacexpr.mli	11833	log plain
-rw-r--r--	tacintern.ml	31386	log plain
-rw-r--r--	tacintern.mli	2068	log plain
-rw-r--r--	tacinterp.ml	82313	log plain
-rw-r--r--	tacinterp.mli	5142	log plain
-rw-r--r--	tacsubst.ml	12569	log plain
-rw-r--r--	tacsubst.mli	1117	log plain
-rw-r--r--	tactic_debug.ml	14895	log plain
-rw-r--r--	tactic_debug.mli	3165	log plain
-rw-r--r--	tactic_matching.ml	15069	log plain
-rw-r--r--	tactic_matching.mli	2227	log plain
-rw-r--r--	tactic_option.ml	1971	log plain
-rw-r--r--	tactic_option.mli	799	log plain
-rw-r--r--	tauto.ml	9838	log plain
-rw-r--r--	tauto.mli	0	log plain
-rw-r--r--	tauto_plugin.mlpack	6	log plain