ltac « plugins - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Ltac.v	0	log plain
-rw-r--r--	coretactics.ml4	10183	log plain
-rw-r--r--	evar_tactics.ml	3984	log plain
-rw-r--r--	evar_tactics.mli	932	log plain
-rw-r--r--	extraargs.ml4	13383	log plain
-rw-r--r--	extraargs.mli	2605	log plain
-rw-r--r--	extratactics.ml4	39079	log plain
-rw-r--r--	extratactics.mli	811	log plain
-rw-r--r--	g_auto.ml4	7042	log plain
-rw-r--r--	g_class.ml4	3854	log plain
-rw-r--r--	g_eqdecide.ml4	1116	log plain
-rw-r--r--	g_ltac.ml4	19041	log plain
-rw-r--r--	g_obligations.ml4	5579	log plain
-rw-r--r--	g_rewrite.ml4	13014	log plain
-rw-r--r--	g_tactic.ml4	28538	log plain
-rw-r--r--	ltac_plugin.mlpack	278	log plain
-rw-r--r--	pltac.ml	2514	log plain
-rw-r--r--	pltac.mli	1709	log plain
-rw-r--r--	pptactic.ml	52759	log plain
-rw-r--r--	pptactic.mli	4866	log plain
-rw-r--r--	profile_ltac.ml	15762	log plain
-rw-r--r--	profile_ltac.mli	3916	log plain
-rw-r--r--	profile_ltac_tactics.ml4	2679	log plain
-rw-r--r--	rewrite.ml	84823	log plain
-rw-r--r--	rewrite.mli	3522	log plain
-rw-r--r--	tacarg.ml	929	log plain
-rw-r--r--	tacarg.mli	1177	log plain
-rw-r--r--	taccoerce.ml	11555	log plain
-rw-r--r--	taccoerce.mli	3245	log plain
-rw-r--r--	tacentries.ml	19120	log plain
-rw-r--r--	tacentries.mli	2862	log plain
-rw-r--r--	tacenv.ml	5228	log plain
-rw-r--r--	tacenv.mli	3136	log plain
-rw-r--r--	tacexpr.mli	11783	log plain
-rw-r--r--	tacintern.ml	32164	log plain
-rw-r--r--	tacintern.mli	2008	log plain
-rw-r--r--	tacinterp.ml	83048	log plain
-rw-r--r--	tacinterp.mli	5309	log plain
-rw-r--r--	tacsubst.ml	12609	log plain
-rw-r--r--	tacsubst.mli	1108	log plain
-rw-r--r--	tactic_debug.ml	15043	log plain
-rw-r--r--	tactic_debug.mli	3120	log plain
-rw-r--r--	tactic_matching.ml	15048	log plain
-rw-r--r--	tactic_matching.mli	2223	log plain
-rw-r--r--	tactic_option.ml	1962	log plain
-rw-r--r--	tactic_option.mli	781	log plain
-rw-r--r--	tauto.ml	9830	log plain
-rw-r--r--	tauto.mli	0	log plain
-rw-r--r--	tauto_plugin.mlpack	6	log plain