ltac - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	autorewrite.ml	11411	log plain
-rw-r--r--	autorewrite.mli	2171	log plain
-rw-r--r--	coretactics.ml4	8223	log plain
-rw-r--r--	eqdecide.ml	7501	log plain
-rw-r--r--	eqdecide.mli	1007	log plain
-rw-r--r--	evar_tactics.ml	3144	log plain
-rw-r--r--	evar_tactics.mli	883	log plain
-rw-r--r--	extraargs.ml4	10979	log plain
-rw-r--r--	extraargs.mli	2245	log plain
-rw-r--r--	extratactics.ml4	35725	log plain
-rw-r--r--	extratactics.mli	810	log plain
-rw-r--r--	g_auto.ml4	6397	log plain
-rw-r--r--	g_class.ml4	2778	log plain
-rw-r--r--	g_eqdecide.ml4	1158	log plain
-rw-r--r--	g_ltac.ml4	15516	log plain
-rw-r--r--	g_obligations.ml4	5151	log plain
-rw-r--r--	g_rewrite.ml4	12564	log plain
-rw-r--r--	ltac.mllib	214	log plain
-rw-r--r--	rewrite.ml	82004	log plain
-rw-r--r--	rewrite.mli	3397	log plain
-rw-r--r--	tacentries.ml	9239	log plain
-rw-r--r--	tacentries.mli	906	log plain
-rw-r--r--	tacenv.ml	4381	log plain
-rw-r--r--	tacenv.mli	2769	log plain
-rw-r--r--	tacintern.ml	31284	log plain
-rw-r--r--	tacintern.mli	2012	log plain
-rw-r--r--	tacinterp.ml	84259	log plain
-rw-r--r--	tacinterp.mli	4236	log plain
-rw-r--r--	tacsubst.ml	12606	log plain
-rw-r--r--	tacsubst.mli	1108	log plain
-rw-r--r--	tactic_debug.ml	14035	log plain
-rw-r--r--	tactic_debug.mli	3108	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	9607	log plain
-rw-r--r--	tauto.mli	0	log plain