kernel - coq - the Coq proof assistant

Mode	Name	Size
d---------	byterun	526	log plain
-rw-r--r--	cbytecodes.ml	10129	log plain
-rw-r--r--	cbytecodes.mli	6132	log plain
-rw-r--r--	cbytegen.ml	36047	log plain
-rw-r--r--	cbytegen.mli	1823	log plain
-rw-r--r--	cemitcodes.ml	12091	log plain
-rw-r--r--	cemitcodes.mli	1045	log plain
-rw-r--r--	closure.ml	36530	log plain
-rw-r--r--	closure.mli	7731	log plain
-rw-r--r--	constr.ml	37404	log plain
-rw-r--r--	constr.mli	12048	log plain
-rw-r--r--	context.ml	4950	log plain
-rw-r--r--	context.mli	4705	log plain
-rw-r--r--	conv_oracle.ml	3094	log plain
-rw-r--r--	conv_oracle.mli	1697	log plain
-rw-r--r--	cooking.ml	8493	log plain
-rw-r--r--	cooking.mli	1087	log plain
-rw-r--r--	csymtable.ml	7529	log plain
-rw-r--r--	csymtable.mli	708	log plain
-rw-r--r--	declarations.mli	10173	log plain
-rw-r--r--	declareops.ml	11530	log plain
-rw-r--r--	declareops.mli	3273	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	entries.mli	3642	log plain
-rw-r--r--	environ.ml	22571	log plain
-rw-r--r--	environ.mli	10517	log plain
-rw-r--r--	esubst.ml	5783	log plain
-rw-r--r--	esubst.mli	2865	log plain
-rw-r--r--	evar.ml	690	log plain
-rw-r--r--	evar.mli	1322	log plain
-rw-r--r--	fast_typeops.ml	14762	log plain
-rw-r--r--	fast_typeops.mli	1134	log plain
-rw-r--r--	indtypes.ml	34761	log plain
-rw-r--r--	indtypes.mli	1721	log plain
-rw-r--r--	inductive.ml	45348	log plain
-rw-r--r--	inductive.mli	5339	log plain
-rw-r--r--	kernel.mllib	421	log plain
-rw-r--r--	make-opcodes	102	log plain
-rw-r--r--	mod_subst.ml	18020	log plain
-rw-r--r--	mod_subst.mli	5833	log plain
-rw-r--r--	mod_typing.ml	12164	log plain
-rw-r--r--	mod_typing.mli	1713	log plain
-rw-r--r--	modops.ml	21888	log plain
-rw-r--r--	modops.mli	5037	log plain
-rw-r--r--	names.ml	23851	log plain
-rw-r--r--	names.mli	20173	log plain
-rw-r--r--	nativecode.ml	73562	log plain
-rw-r--r--	nativecode.mli	2284	log plain
-rw-r--r--	nativeconv.ml	5492	log plain
-rw-r--r--	nativeconv.mli	711	log plain
-rw-r--r--	nativeinstr.mli	2211	log plain
-rw-r--r--	nativelambda.ml	24566	log plain
-rw-r--r--	nativelambda.mli	1551	log plain
-rw-r--r--	nativelib.ml	4588	log plain
-rw-r--r--	nativelib.mli	1214	log plain
-rw-r--r--	nativelibrary.ml	2684	log plain
-rw-r--r--	nativelibrary.mli	773	log plain
-rw-r--r--	nativevalues.ml	16104	log plain
-rw-r--r--	nativevalues.mli	4903	log plain
-rw-r--r--	opaqueproof.ml	5201	log plain
-rw-r--r--	opaqueproof.mli	3325	log plain
-rw-r--r--	pre_env.ml	5030	log plain
-rw-r--r--	pre_env.mli	2657	log plain
-rw-r--r--	primitives.ml	2031	log plain
-rw-r--r--	primitives.mli	938	log plain
-rw-r--r--	reduction.ml	30200	log plain
-rw-r--r--	reduction.mli	5057	log plain
-rw-r--r--	retroknowledge.ml	7464	log plain
-rw-r--r--	retroknowledge.mli	6866	log plain
-rw-r--r--	safe_typing.ml	30022	log plain
-rw-r--r--	safe_typing.mli	5702	log plain
-rw-r--r--	sorts.ml	2595	log plain
-rw-r--r--	sorts.mli	1198	log plain
-rw-r--r--	subtyping.ml	19545	log plain
-rw-r--r--	subtyping.mli	650	log plain
-rw-r--r--	term.ml	22004	log plain
-rw-r--r--	term.mli	16247	log plain
-rw-r--r--	term_typing.ml	12112	log plain
-rw-r--r--	term_typing.mli	1931	log plain
-rw-r--r--	type_errors.ml	4234	log plain
-rw-r--r--	type_errors.mli	3824	log plain
-rw-r--r--	typeops.ml	18009	log plain
-rw-r--r--	typeops.mli	4464	log plain
-rw-r--r--	uint31.ml	4093	log plain
-rw-r--r--	uint31.mli	912	log plain
-rw-r--r--	univ.ml	61331	log plain
-rw-r--r--	univ.mli	13798	log plain
-rw-r--r--	vars.ml	10572	log plain
-rw-r--r--	vars.mli	3796	log plain
-rw-r--r--	vconv.ml	8773	log plain
-rw-r--r--	vconv.mli	816	log plain
-rw-r--r--	vm.ml	20380	log plain
-rw-r--r--	vm.mli	2262	log plain