kernel - coq - The formal proof system

Mode	Name	Size
d---------	byterun	519	log plain
-rw-r--r--	cClosure.ml	39043	log plain
-rw-r--r--	cClosure.mli	8401	log plain
-rw-r--r--	cPrimitives.ml	2181	log plain
-rw-r--r--	cPrimitives.mli	1088	log plain
-rw-r--r--	cbytecodes.ml	9598	log plain
-rw-r--r--	cbytecodes.mli	6335	log plain
-rw-r--r--	cbytegen.ml	35690	log plain
-rw-r--r--	cbytegen.mli	1280	log plain
-rw-r--r--	cemitcodes.ml	15893	log plain
-rw-r--r--	cemitcodes.mli	858	log plain
-rw-r--r--	cinstr.mli	2183	log plain
-rw-r--r--	clambda.ml	27727	log plain
-rw-r--r--	clambda.mli	1227	log plain
-rw-r--r--	constr.ml	48975	log plain
-rw-r--r--	constr.mli	24428	log plain
-rw-r--r--	context.ml	17384	log plain
-rw-r--r--	context.mli	12423	log plain
-rw-r--r--	conv_oracle.ml	3403	log plain
-rw-r--r--	conv_oracle.mli	1855	log plain
-rw-r--r--	cooking.ml	8793	log plain
-rw-r--r--	cooking.mli	1250	log plain
-rw-r--r--	csymtable.ml	6136	log plain
-rw-r--r--	csymtable.mli	923	log plain
-rw-r--r--	declarations.ml	11379	log plain
-rw-r--r--	declareops.ml	13116	log plain
-rw-r--r--	declareops.mli	3005	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	dune	484	log plain
-rw-r--r--	entries.ml	4628	log plain
-rw-r--r--	environ.ml	22079	log plain
-rw-r--r--	environ.mli	11980	log plain
-rw-r--r--	esubst.ml	6859	log plain
-rw-r--r--	esubst.mli	3437	log plain
-rw-r--r--	evar.ml	877	log plain
-rw-r--r--	evar.mli	1526	log plain
-rw-r--r--	indtypes.ml	40278	log plain
-rw-r--r--	indtypes.mli	1680	log plain
-rw-r--r--	inductive.ml	46706	log plain
-rw-r--r--	inductive.mli	5410	log plain
-rw-r--r--	kernel.mllib	435	log plain
-rw-r--r--	make-opcodes	170	log plain
-rwxr-xr-x	make_opcodes.sh	162	log plain
-rw-r--r--	mod_subst.ml	17984	log plain
-rw-r--r--	mod_subst.mli	5997	log plain
-rw-r--r--	mod_typing.ml	14309	log plain
-rw-r--r--	mod_typing.mli	2373	log plain
-rw-r--r--	modops.ml	22659	log plain
-rw-r--r--	modops.mli	5134	log plain
-rw-r--r--	names.ml	31551	log plain
-rw-r--r--	names.mli	18828	log plain
-rw-r--r--	nativecode.ml	75792	log plain
-rw-r--r--	nativecode.mli	2517	log plain
-rw-r--r--	nativeconv.ml	7143	log plain
-rw-r--r--	nativeconv.mli	1053	log plain
-rw-r--r--	nativeinstr.mli	2665	log plain
-rw-r--r--	nativelambda.ml	21971	log plain
-rw-r--r--	nativelambda.mli	1656	log plain
-rw-r--r--	nativelib.ml	6054	log plain
-rw-r--r--	nativelib.mli	1381	log plain
-rw-r--r--	nativelibrary.ml	2842	log plain
-rw-r--r--	nativelibrary.mli	917	log plain
-rw-r--r--	nativevalues.ml	15443	log plain
-rw-r--r--	nativevalues.mli	5059	log plain
-rw-r--r--	opaqueproof.ml	6061	log plain
-rw-r--r--	opaqueproof.mli	3457	log plain
-rw-r--r--	reduction.ml	35334	log plain
-rw-r--r--	reduction.mli	5589	log plain
-rw-r--r--	retroknowledge.ml	7893	log plain
-rw-r--r--	retroknowledge.mli	6437	log plain
-rw-r--r--	safe_typing.ml	39069	log plain
-rw-r--r--	safe_typing.mli	7430	log plain
-rw-r--r--	sorts.ml	2600	log plain
-rw-r--r--	sorts.mli	1287	log plain
-rw-r--r--	subtyping.ml	15294	log plain
-rw-r--r--	subtyping.mli	799	log plain
-rw-r--r--	term.ml	13551	log plain
-rw-r--r--	term.mli	8061	log plain
-rw-r--r--	term_typing.ml	22894	log plain
-rw-r--r--	term_typing.mli	2945	log plain
-rw-r--r--	type_errors.ml	4920	log plain
-rw-r--r--	type_errors.mli	4453	log plain
-rw-r--r--	typeops.ml	17745	log plain
-rw-r--r--	typeops.mli	3761	log plain
-rw-r--r--	uGraph.ml	31802	log plain
-rw-r--r--	uGraph.mli	3375	log plain
-rw-r--r--	uint31.ml	4093	log plain
-rw-r--r--	uint31.mli	912	log plain
-rw-r--r--	univ.ml	33932	log plain
-rw-r--r--	univ.mli	16748	log plain
-rw-r--r--	vars.ml	9910	log plain
-rw-r--r--	vars.mli	6702	log plain
-rw-r--r--	vconv.ml	7862	log plain
-rw-r--r--	vconv.mli	1032	log plain
-rw-r--r--	vm.ml	5961	log plain
-rw-r--r--	vm.mli	1446	log plain
-rw-r--r--	vmvalues.ml	22971	log plain
-rw-r--r--	vmvalues.mli	4875	log plain