kernel - coq - The formal proof system

Mode	Name	Size
d---------	byterun	519	log plain
-rw-r--r--	cClosure.ml	39033	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	9596	log plain
-rw-r--r--	cbytecodes.mli	6335	log plain
-rw-r--r--	cbytegen.ml	35455	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	27572	log plain
-rw-r--r--	clambda.mli	1227	log plain
-rw-r--r--	constr.ml	48948	log plain
-rw-r--r--	constr.mli	24479	log plain
-rw-r--r--	context.ml	17380	log plain
-rw-r--r--	context.mli	12423	log plain
-rw-r--r--	conv_oracle.ml	3392	log plain
-rw-r--r--	conv_oracle.mli	1855	log plain
-rw-r--r--	cooking.ml	8792	log plain
-rw-r--r--	cooking.mli	1250	log plain
-rw-r--r--	csymtable.ml	6133	log plain
-rw-r--r--	csymtable.mli	923	log plain
-rw-r--r--	declarations.ml	11379	log plain
-rw-r--r--	declareops.ml	13111	log plain
-rw-r--r--	declareops.mli	3005	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	dune	359	log plain
-rw-r--r--	entries.ml	4628	log plain
-rw-r--r--	environ.ml	21922	log plain
-rw-r--r--	environ.mli	11991	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	40304	log plain
-rw-r--r--	indtypes.mli	1680	log plain
-rw-r--r--	inductive.ml	46653	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	17983	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	22634	log plain
-rw-r--r--	modops.mli	5134	log plain
-rw-r--r--	names.ml	31545	log plain
-rw-r--r--	names.mli	18828	log plain
-rw-r--r--	nativecode.ml	75776	log plain
-rw-r--r--	nativecode.mli	2517	log plain
-rw-r--r--	nativeconv.ml	7139	log plain
-rw-r--r--	nativeconv.mli	1053	log plain
-rw-r--r--	nativeinstr.mli	2665	log plain
-rw-r--r--	nativelambda.ml	21863	log plain
-rw-r--r--	nativelambda.mli	1656	log plain
-rw-r--r--	nativelib.ml	6050	log plain
-rw-r--r--	nativelib.mli	1381	log plain
-rw-r--r--	nativelibrary.ml	2835	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	6040	log plain
-rw-r--r--	opaqueproof.mli	3457	log plain
-rw-r--r--	reduction.ml	35300	log plain
-rw-r--r--	reduction.mli	5589	log plain
-rw-r--r--	retroknowledge.ml	7197	log plain
-rw-r--r--	retroknowledge.mli	6373	log plain
-rw-r--r--	safe_typing.ml	39235	log plain
-rw-r--r--	safe_typing.mli	7458	log plain
-rw-r--r--	sorts.ml	2600	log plain
-rw-r--r--	sorts.mli	1287	log plain
-rw-r--r--	subtyping.ml	15140	log plain
-rw-r--r--	subtyping.mli	799	log plain
-rw-r--r--	term.ml	13545	log plain
-rw-r--r--	term.mli	8061	log plain
-rw-r--r--	term_typing.ml	22857	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	4457	log plain
-rw-r--r--	typeops.ml	17732	log plain
-rw-r--r--	typeops.mli	3761	log plain
-rw-r--r--	uGraph.ml	31790	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	34038	log plain
-rw-r--r--	univ.mli	16748	log plain
-rw-r--r--	vars.ml	9908	log plain
-rw-r--r--	vars.mli	6702	log plain
-rw-r--r--	vconv.ml	7859	log plain
-rw-r--r--	vconv.mli	1032	log plain
-rw-r--r--	vm.ml	5960	log plain
-rw-r--r--	vm.mli	1446	log plain
-rw-r--r--	vmvalues.ml	22686	log plain
-rw-r--r--	vmvalues.mli	4903	log plain