ltac « plugins - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	Ltac.v	0	log plain
-rw-r--r--	coretactics.ml4	9150	log plain
-rw-r--r--	evar_tactics.ml	4061	log plain
-rw-r--r--	evar_tactics.mli	932	log plain
-rw-r--r--	extraargs.ml4	12718	log plain
-rw-r--r--	extraargs.mli	2556	log plain
-rw-r--r--	extratactics.ml4	37897	log plain
-rw-r--r--	extratactics.mli	810	log plain
-rw-r--r--	g_auto.ml4	7019	log plain
-rw-r--r--	g_class.ml4	3963	log plain
-rw-r--r--	g_eqdecide.ml4	1169	log plain
-rw-r--r--	g_ltac.ml4	19226	log plain
-rw-r--r--	g_obligations.ml4	5636	log plain
-rw-r--r--	g_rewrite.ml4	12599	log plain
-rw-r--r--	g_tactic.ml4	26081	log plain
-rw-r--r--	ltac_plugin.mlpack	284	log plain
-rw-r--r--	pltac.ml	2525	log plain
-rw-r--r--	pltac.mli	1758	log plain
-rw-r--r--	pptactic.ml	48938	log plain
-rw-r--r--	pptactic.mli	3937	log plain
-rw-r--r--	profile_ltac.ml	14509	log plain
-rw-r--r--	profile_ltac.mli	1860	log plain
-rw-r--r--	profile_ltac_tactics.ml4	1474	log plain
-rw-r--r--	rewrite.ml	85021	log plain
-rw-r--r--	rewrite.mli	3553	log plain
-rw-r--r--	tacarg.ml	929	log plain
-rw-r--r--	tacarg.mli	1177	log plain
-rw-r--r--	taccoerce.ml	11596	log plain
-rw-r--r--	taccoerce.mli	3311	log plain
-rw-r--r--	tacentries.ml	18002	log plain
-rw-r--r--	tacentries.mli	2754	log plain
-rw-r--r--	tacenv.ml	4286	log plain
-rw-r--r--	tacenv.mli	2784	log plain
-rw-r--r--	tacexpr.mli	11846	log plain
-rw-r--r--	tacintern.ml	31384	log plain
-rw-r--r--	tacintern.mli	2012	log plain
-rw-r--r--	tacinterp.ml	84018	log plain
-rw-r--r--	tacinterp.mli	4427	log plain
-rw-r--r--	tacsubst.ml	12570	log plain
-rw-r--r--	tacsubst.mli	1108	log plain
-rw-r--r--	tactic_debug.ml	14618	log plain
-rw-r--r--	tactic_debug.mli	3166	log plain
-rw-r--r--	tactic_matching.ml	15060	log plain
-rw-r--r--	tactic_matching.mli	2217	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	9930	log plain
-rw-r--r--	tauto.mli	0	log plain
-rw-r--r--	vo.itarget	8	log plain