ltac « plugins - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Ltac.v	0	log plain
-rw-r--r--	coretactics.ml4	10567	log plain
-rw-r--r--	evar_tactics.ml	4134	log plain
-rw-r--r--	evar_tactics.mli	1082	log plain
-rw-r--r--	extraargs.ml4	13533	log plain
-rw-r--r--	extraargs.mli	2755	log plain
-rw-r--r--	extratactics.ml4	39420	log plain
-rw-r--r--	extratactics.mli	961	log plain
-rw-r--r--	g_auto.ml4	7192	log plain
-rw-r--r--	g_class.ml4	4004	log plain
-rw-r--r--	g_eqdecide.ml4	1278	log plain
-rw-r--r--	g_ltac.ml4	19274	log plain
-rw-r--r--	g_obligations.ml4	5731	log plain
-rw-r--r--	g_rewrite.ml4	13164	log plain
-rw-r--r--	g_tactic.ml4	28796	log plain
-rw-r--r--	ltac_plugin.mlpack	286	log plain
-rw-r--r--	pltac.ml	2664	log plain
-rw-r--r--	pltac.mli	1857	log plain
-rw-r--r--	pptactic.ml	52983	log plain
-rw-r--r--	pptactic.mli	5027	log plain
-rw-r--r--	profile_ltac.ml	15912	log plain
-rw-r--r--	profile_ltac.mli	4066	log plain
-rw-r--r--	profile_ltac_tactics.ml4	2829	log plain
-rw-r--r--	rewrite.ml	85148	log plain
-rw-r--r--	rewrite.mli	3672	log plain
-rw-r--r--	tacarg.ml	1079	log plain
-rw-r--r--	tacarg.mli	1327	log plain
-rw-r--r--	taccoerce.ml	14591	log plain
-rw-r--r--	taccoerce.mli	4154	log plain
-rw-r--r--	tacentries.ml	24649	log plain
-rw-r--r--	tacentries.mli	3454	log plain
-rw-r--r--	tacenv.ml	5378	log plain
-rw-r--r--	tacenv.mli	3286	log plain
-rw-r--r--	tacexpr.ml	12182	log plain
-rw-r--r--	tacexpr.mli	12182	log plain
-rw-r--r--	tacintern.ml	32227	log plain
-rw-r--r--	tacintern.mli	2158	log plain
-rw-r--r--	tacinterp.ml	79960	log plain
-rw-r--r--	tacinterp.mli	5075	log plain
-rw-r--r--	tacsubst.ml	12785	log plain
-rw-r--r--	tacsubst.mli	1258	log plain
-rw-r--r--	tactic_debug.ml	15003	log plain
-rw-r--r--	tactic_debug.mli	3270	log plain
-rw-r--r--	tactic_matching.ml	15198	log plain
-rw-r--r--	tactic_matching.mli	2372	log plain
-rw-r--r--	tactic_option.ml	2112	log plain
-rw-r--r--	tactic_option.mli	931	log plain
-rw-r--r--	tauto.ml	9472	log plain
-rw-r--r--	tauto.mli	0	log plain
-rw-r--r--	tauto_plugin.mlpack	6	log plain