kernel - coq - the Coq proof assistant

Mode	Name	Size
d---------	byterun	526	log plain
-rw-r--r--	cbytecodes.ml	9888	log plain
-rw-r--r--	cbytecodes.mli	6101	log plain
-rw-r--r--	cbytegen.ml	33415	log plain
-rw-r--r--	cbytegen.mli	1742	log plain
-rw-r--r--	cemitcodes.ml	11971	log plain
-rw-r--r--	cemitcodes.mli	1013	log plain
-rw-r--r--	closure.ml	39189	log plain
-rw-r--r--	closure.mli	7430	log plain
-rw-r--r--	constr.ml	37311	log plain
-rw-r--r--	constr.mli	11463	log plain
-rw-r--r--	context.ml	4474	log plain
-rw-r--r--	context.mli	4236	log plain
-rw-r--r--	conv_oracle.ml	3032	log plain
-rw-r--r--	conv_oracle.mli	1686	log plain
-rw-r--r--	cooking.ml	7361	log plain
-rw-r--r--	cooking.mli	1087	log plain
-rw-r--r--	csymtable.ml	7232	log plain
-rw-r--r--	csymtable.mli	708	log plain
-rw-r--r--	declarations.mli	9239	log plain
-rw-r--r--	declareops.ml	10332	log plain
-rw-r--r--	declareops.mli	3014	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	entries.mli	3216	log plain
-rw-r--r--	environ.ml	24551	log plain
-rw-r--r--	environ.mli	10386	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	14461	log plain
-rw-r--r--	fast_typeops.mli	1115	log plain
-rw-r--r--	indtypes.ml	29570	log plain
-rw-r--r--	indtypes.mli	1650	log plain
-rw-r--r--	inductive.ml	38574	log plain
-rw-r--r--	inductive.mli	5318	log plain
-rw-r--r--	kernel.mllib	421	log plain
-rw-r--r--	make-opcodes	102	log plain
-rw-r--r--	mod_subst.ml	17985	log plain
-rw-r--r--	mod_subst.mli	5833	log plain
-rw-r--r--	mod_typing.ml	12131	log plain
-rw-r--r--	mod_typing.mli	1915	log plain
-rw-r--r--	modops.ml	21463	log plain
-rw-r--r--	modops.mli	4815	log plain
-rw-r--r--	names.ml	22796	log plain
-rw-r--r--	names.mli	19720	log plain
-rw-r--r--	nativecode.ml	69512	log plain
-rw-r--r--	nativecode.mli	2235	log plain
-rw-r--r--	nativeconv.ml	5463	log plain
-rw-r--r--	nativeconv.mli	711	log plain
-rw-r--r--	nativeinstr.mli	2207	log plain
-rw-r--r--	nativelambda.ml	24296	log plain
-rw-r--r--	nativelambda.mli	1567	log plain
-rw-r--r--	nativelib.ml	4541	log plain
-rw-r--r--	nativelib.mli	1139	log plain
-rw-r--r--	nativelibrary.ml	2699	log plain
-rw-r--r--	nativelibrary.mli	773	log plain
-rw-r--r--	nativevalues.ml	15596	log plain
-rw-r--r--	nativevalues.mli	4835	log plain
-rw-r--r--	opaqueproof.ml	4416	log plain
-rw-r--r--	opaqueproof.mli	3142	log plain
-rw-r--r--	pre_env.ml	4836	log plain
-rw-r--r--	pre_env.mli	2584	log plain
-rw-r--r--	primitives.ml	2031	log plain
-rw-r--r--	primitives.mli	938	log plain
-rw-r--r--	reduction.ml	28984	log plain
-rw-r--r--	reduction.mli	5016	log plain
-rw-r--r--	retroknowledge.ml	11562	log plain
-rw-r--r--	retroknowledge.mli	7430	log plain
-rw-r--r--	safe_typing.ml	28561	log plain
-rw-r--r--	safe_typing.mli	5435	log plain
-rw-r--r--	sorts.ml	2582	log plain
-rw-r--r--	sorts.mli	1198	log plain
-rw-r--r--	subtyping.ml	17511	log plain
-rw-r--r--	subtyping.mli	650	log plain
-rw-r--r--	term.ml	21809	log plain
-rw-r--r--	term.mli	16111	log plain
-rw-r--r--	term_typing.ml	12528	log plain
-rw-r--r--	term_typing.mli	1635	log plain
-rw-r--r--	type_errors.ml	4190	log plain
-rw-r--r--	type_errors.mli	3780	log plain
-rw-r--r--	typeops.ml	18173	log plain
-rw-r--r--	typeops.mli	4464	log plain
-rw-r--r--	uint31.ml	4097	log plain
-rw-r--r--	uint31.mli	912	log plain
-rw-r--r--	univ.ml	60662	log plain
-rw-r--r--	univ.mli	12879	log plain
-rw-r--r--	vars.ml	9387	log plain
-rw-r--r--	vars.mli	3614	log plain
-rw-r--r--	vconv.ml	8434	log plain
-rw-r--r--	vconv.mli	816	log plain
-rw-r--r--	vm.ml	20096	log plain
-rw-r--r--	vm.mli	2249	log plain