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	33073	log plain
-rw-r--r--	cbytegen.mli	1742	log plain
-rw-r--r--	cemitcodes.ml	11967	log plain
-rw-r--r--	cemitcodes.mli	1013	log plain
-rw-r--r--	closure.ml	34428	log plain
-rw-r--r--	closure.mli	6515	log plain
-rw-r--r--	constr.ml	25159	log plain
-rw-r--r--	constr.mli	8572	log plain
-rw-r--r--	context.ml	4467	log plain
-rw-r--r--	context.mli	4238	log plain
-rw-r--r--	conv_oracle.ml	2416	log plain
-rw-r--r--	conv_oracle.mli	1560	log plain
-rw-r--r--	cooking.ml	4749	log plain
-rw-r--r--	cooking.mli	1117	log plain
-rw-r--r--	csymtable.ml	5439	log plain
-rw-r--r--	csymtable.mli	708	log plain
-rw-r--r--	declarations.mli	6829	log plain
-rw-r--r--	declareops.ml	7051	log plain
-rw-r--r--	declareops.mli	1947	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	entries.mli	2780	log plain
-rw-r--r--	environ.ml	17691	log plain
-rw-r--r--	environ.mli	7919	log plain
-rw-r--r--	esubst.ml	5769	log plain
-rw-r--r--	esubst.mli	2865	log plain
-rw-r--r--	indtypes.ml	25823	log plain
-rw-r--r--	indtypes.mli	1397	log plain
-rw-r--r--	inductive.ml	35357	log plain
-rw-r--r--	inductive.mli	4472	log plain
-rw-r--r--	kernel.mllib	373	log plain
-rw-r--r--	lazyconstr.ml	2754	log plain
-rw-r--r--	lazyconstr.mli	2172	log plain
-rw-r--r--	make-opcodes	102	log plain
-rw-r--r--	mod_subst.ml	17197	log plain
-rw-r--r--	mod_subst.mli	5305	log plain
-rw-r--r--	mod_typing.ml	15385	log plain
-rw-r--r--	mod_typing.mli	1722	log plain
-rw-r--r--	modops.ml	20747	log plain
-rw-r--r--	modops.mli	4060	log plain
-rw-r--r--	names.ml	20125	log plain
-rw-r--r--	names.mli	18526	log plain
-rw-r--r--	nativecode.ml	58903	log plain
-rw-r--r--	nativecode.mli	2168	log plain
-rw-r--r--	nativeconv.ml	5466	log plain
-rw-r--r--	nativeconv.mli	707	log plain
-rw-r--r--	nativelambda.ml	21125	log plain
-rw-r--r--	nativelambda.mli	2143	log plain
-rw-r--r--	nativelib.ml	3881	log plain
-rw-r--r--	nativelib.mli	1187	log plain
-rw-r--r--	nativelibrary.ml	2416	log plain
-rw-r--r--	nativelibrary.mli	878	log plain
-rw-r--r--	nativevalues.ml	7407	log plain
-rw-r--r--	nativevalues.mli	2815	log plain
-rw-r--r--	pre_env.ml	3767	log plain
-rw-r--r--	pre_env.mli	2244	log plain
-rw-r--r--	reduction.ml	20820	log plain
-rw-r--r--	reduction.mli	3479	log plain
-rw-r--r--	retroknowledge.ml	8520	log plain
-rw-r--r--	retroknowledge.mli	5938	log plain
-rw-r--r--	safe_typing.ml	24822	log plain
-rw-r--r--	safe_typing.mli	4427	log plain
-rw-r--r--	sorts.ml	1737	log plain
-rw-r--r--	sorts.mli	883	log plain
-rw-r--r--	subtyping.ml	16831	log plain
-rw-r--r--	subtyping.mli	650	log plain
-rw-r--r--	term.ml	20826	log plain
-rw-r--r--	term.mli	14637	log plain
-rw-r--r--	term_typing.ml	4462	log plain
-rw-r--r--	term_typing.mli	1182	log plain
-rw-r--r--	type_errors.ml	4026	log plain
-rw-r--r--	type_errors.mli	3661	log plain
-rw-r--r--	typeops.ml	16372	log plain
-rw-r--r--	typeops.mli	3713	log plain
-rw-r--r--	univ.ml	34257	log plain
-rw-r--r--	univ.mli	5234	log plain
-rw-r--r--	vars.ml	6102	log plain
-rw-r--r--	vars.mli	2965	log plain
-rw-r--r--	vconv.ml	7862	log plain
-rw-r--r--	vconv.mli	827	log plain
-rw-r--r--	vm.ml	19786	log plain
-rw-r--r--	vm.mli	2265	log plain