ltac « plugins - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	Ltac.v	0	log plain
-rw-r--r--	coretactics.mlg	10551	log plain
-rw-r--r--	evar_tactics.ml	4152	log plain
-rw-r--r--	evar_tactics.mli	1082	log plain
-rw-r--r--	extraargs.mlg	9599	log plain
-rw-r--r--	extraargs.mli	2580	log plain
-rw-r--r--	extratactics.mlg	35980	log plain
-rw-r--r--	extratactics.mli	962	log plain
-rw-r--r--	g_auto.mlg	7439	log plain
-rw-r--r--	g_class.mlg	4360	log plain
-rw-r--r--	g_eqdecide.mlg	1284	log plain
-rw-r--r--	g_ltac.mlg	19682	log plain
-rw-r--r--	g_obligations.mlg	5779	log plain
-rw-r--r--	g_rewrite.mlg	13521	log plain
-rw-r--r--	g_tactic.mlg	29859	log plain
-rw-r--r--	ltac_plugin.mlpack	286	log plain
-rw-r--r--	pltac.ml	2574	log plain
-rw-r--r--	pltac.mli	1817	log plain
-rw-r--r--	plugin_base.dune	298	log plain
-rw-r--r--	pptactic.ml	55190	log plain
-rw-r--r--	pptactic.mli	5975	log plain
-rw-r--r--	profile_ltac.ml	15913	log plain
-rw-r--r--	profile_ltac.mli	4066	log plain
-rw-r--r--	profile_ltac_tactics.mlg	2841	log plain
-rw-r--r--	rewrite.ml	86147	log plain
-rw-r--r--	rewrite.mli	3893	log plain
-rw-r--r--	tacarg.ml	1416	log plain
-rw-r--r--	tacarg.mli	2271	log plain
-rw-r--r--	taccoerce.ml	14729	log plain
-rw-r--r--	taccoerce.mli	4037	log plain
-rw-r--r--	tacentries.ml	27677	log plain
-rw-r--r--	tacentries.mli	5642	log plain
-rw-r--r--	tacenv.ml	5928	log plain
-rw-r--r--	tacenv.mli	3643	log plain
-rw-r--r--	tacexpr.ml	11076	log plain
-rw-r--r--	tacexpr.mli	11075	log plain
-rw-r--r--	tacintern.ml	33779	log plain
-rw-r--r--	tacintern.mli	2174	log plain
-rw-r--r--	tacinterp.ml	82434	log plain
-rw-r--r--	tacinterp.mli	5164	log plain
-rw-r--r--	tacsubst.ml	12594	log plain
-rw-r--r--	tacsubst.mli	1272	log plain
-rw-r--r--	tactic_debug.ml	15157	log plain
-rw-r--r--	tactic_debug.mli	3281	log plain
-rw-r--r--	tactic_matching.ml	15242	log plain
-rw-r--r--	tactic_matching.mli	2388	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	9765	log plain
-rw-r--r--	tauto.mli	0	log plain
-rw-r--r--	tauto_plugin.mlpack	6	log plain