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	33113	log plain
-rw-r--r--	cbytegen.mli	1742	log plain
-rw-r--r--	cemitcodes.ml	12006	log plain
-rw-r--r--	cemitcodes.mli	1013	log plain
-rw-r--r--	closure.ml	34400	log plain
-rw-r--r--	closure.mli	6507	log plain
-rw-r--r--	conv_oracle.ml	2487	log plain
-rw-r--r--	conv_oracle.mli	1588	log plain
-rw-r--r--	cooking.ml	4579	log plain
-rw-r--r--	cooking.mli	1053	log plain
-rw-r--r--	csymtable.ml	5323	log plain
-rw-r--r--	csymtable.mli	708	log plain
-rw-r--r--	declarations.ml	13324	log plain
-rw-r--r--	declarations.mli	8120	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	entries.mli	2708	log plain
-rw-r--r--	environ.ml	17520	log plain
-rw-r--r--	environ.mli	7916	log plain
-rw-r--r--	esubst.ml	5769	log plain
-rw-r--r--	esubst.mli	2865	log plain
-rw-r--r--	indtypes.ml	25710	log plain
-rw-r--r--	indtypes.mli	1397	log plain
-rw-r--r--	inductive.ml	35226	log plain
-rw-r--r--	inductive.mli	4445	log plain
-rw-r--r--	kernel.mllib	271	log plain
-rw-r--r--	make-opcodes	102	log plain
-rw-r--r--	mod_subst.ml	17334	log plain
-rw-r--r--	mod_subst.mli	5105	log plain
-rw-r--r--	mod_typing.ml	15371	log plain
-rw-r--r--	mod_typing.mli	1722	log plain
-rw-r--r--	modops.ml	20619	log plain
-rw-r--r--	modops.mli	3997	log plain
-rw-r--r--	names.ml	17108	log plain
-rw-r--r--	names.mli	10925	log plain
-rw-r--r--	pre_env.ml	3750	log plain
-rw-r--r--	pre_env.mli	2241	log plain
-rw-r--r--	reduction.ml	20377	log plain
-rw-r--r--	reduction.mli	3344	log plain
-rw-r--r--	retroknowledge.ml	8520	log plain
-rw-r--r--	retroknowledge.mli	5938	log plain
-rw-r--r--	safe_typing.ml	28372	log plain
-rw-r--r--	safe_typing.mli	4674	log plain
-rw-r--r--	sign.ml	2947	log plain
-rw-r--r--	sign.mli	2454	log plain
-rw-r--r--	subtyping.ml	16600	log plain
-rw-r--r--	subtyping.mli	650	log plain
-rw-r--r--	term.ml	50298	log plain
-rw-r--r--	term.mli	22405	log plain
-rw-r--r--	term_typing.ml	5334	log plain
-rw-r--r--	term_typing.mli	1318	log plain
-rw-r--r--	type_errors.ml	4001	log plain
-rw-r--r--	type_errors.mli	3622	log plain
-rw-r--r--	typeops.ml	16482	log plain
-rw-r--r--	typeops.mli	3686	log plain
-rw-r--r--	univ.ml	33799	log plain
-rw-r--r--	univ.mli	5173	log plain
-rw-r--r--	vconv.ml	7862	log plain
-rw-r--r--	vconv.mli	827	log plain
-rw-r--r--	vm.ml	19795	log plain
-rw-r--r--	vm.mli	2265	log plain