src - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	g_ltac2.ml4	27620	log plain
-rw-r--r--	ltac2_plugin.mlpack	128	log plain
-rw-r--r--	tac2core.ml	38884	log plain
-rw-r--r--	tac2core.mli	945	log plain
-rw-r--r--	tac2dyn.ml	951	log plain
-rw-r--r--	tac2dyn.mli	1215	log plain
-rw-r--r--	tac2entries.ml	29084	log plain
-rw-r--r--	tac2entries.mli	2906	log plain
-rw-r--r--	tac2env.ml	8022	log plain
-rw-r--r--	tac2env.mli	4851	log plain
-rw-r--r--	tac2expr.mli	5351	log plain
-rw-r--r--	tac2ffi.ml	9048	log plain
-rw-r--r--	tac2ffi.mli	5434	log plain
-rw-r--r--	tac2intern.ml	50664	log plain
-rw-r--r--	tac2intern.mli	1998	log plain
-rw-r--r--	tac2interp.ml	7299	log plain
-rw-r--r--	tac2interp.mli	1251	log plain
-rw-r--r--	tac2match.ml	8807	log plain
-rw-r--r--	tac2match.mli	1199	log plain
-rw-r--r--	tac2print.ml	14375	log plain
-rw-r--r--	tac2print.mli	1561	log plain
-rw-r--r--	tac2qexpr.mli	4658	log plain
-rw-r--r--	tac2quote.ml	15937	log plain
-rw-r--r--	tac2quote.mli	3271	log plain
-rw-r--r--	tac2stdlib.ml	21950	log plain
-rw-r--r--	tac2stdlib.mli	590	log plain
-rw-r--r--	tac2tactics.ml	15056	log plain
-rw-r--r--	tac2tactics.mli	4561	log plain
-rw-r--r--	tac2types.mli	2510	log plain