kernel - coq - the Coq proof assistant

Mode	Name	Size
d---------	byterun	444	log plain
-rw-r--r--	cClosure.ml	37589	log plain
-rw-r--r--	cClosure.mli	7952	log plain
-rw-r--r--	cPrimitives.ml	2031	log plain
-rw-r--r--	cPrimitives.mli	938	log plain
-rw-r--r--	cbytecodes.ml	11049	log plain
-rw-r--r--	cbytecodes.mli	7367	log plain
-rw-r--r--	cbytegen.ml	42476	log plain
-rw-r--r--	cbytegen.mli	2445	log plain
-rw-r--r--	cemitcodes.ml	13446	log plain
-rw-r--r--	cemitcodes.mli	992	log plain
-rw-r--r--	constr.ml	44020	log plain
-rw-r--r--	constr.mli	18548	log plain
-rw-r--r--	context.ml	17115	log plain
-rw-r--r--	context.mli	12024	log plain
-rw-r--r--	conv_oracle.ml	3242	log plain
-rw-r--r--	conv_oracle.mli	1705	log plain
-rw-r--r--	cooking.ml	8319	log plain
-rw-r--r--	cooking.mli	1153	log plain
-rw-r--r--	csymtable.ml	7357	log plain
-rw-r--r--	csymtable.mli	714	log plain
-rw-r--r--	declarations.ml	10997	log plain
-rw-r--r--	declareops.ml	12786	log plain
-rw-r--r--	declareops.mli	2676	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	entries.ml	4403	log plain
-rw-r--r--	environ.ml	22556	log plain
-rw-r--r--	environ.mli	10385	log plain
-rw-r--r--	esubst.ml	5783	log plain
-rw-r--r--	esubst.mli	2865	log plain
-rw-r--r--	evar.ml	727	log plain
-rw-r--r--	evar.mli	1376	log plain
-rw-r--r--	indtypes.ml	41590	log plain
-rw-r--r--	indtypes.mli	1722	log plain
-rw-r--r--	inductive.ml	46528	log plain
-rw-r--r--	inductive.mli	5239	log plain
-rw-r--r--	kernel.mllib	426	log plain
-rw-r--r--	make-opcodes	170	log plain
-rw-r--r--	mod_subst.ml	18153	log plain
-rw-r--r--	mod_subst.mli	5818	log plain
-rw-r--r--	mod_typing.ml	14559	log plain
-rw-r--r--	mod_typing.mli	2223	log plain
-rw-r--r--	modops.ml	22420	log plain
-rw-r--r--	modops.mli	5021	log plain
-rw-r--r--	names.ml	27238	log plain
-rw-r--r--	names.mli	23590	log plain
-rw-r--r--	nativecode.ml	73698	log plain
-rw-r--r--	nativecode.mli	2332	log plain
-rw-r--r--	nativeconv.ml	6752	log plain
-rw-r--r--	nativeconv.mli	903	log plain
-rw-r--r--	nativeinstr.mli	2224	log plain
-rw-r--r--	nativelambda.ml	21624	log plain
-rw-r--r--	nativelambda.mli	1539	log plain
-rw-r--r--	nativelib.ml	5941	log plain
-rw-r--r--	nativelib.mli	1231	log plain
-rw-r--r--	nativelibrary.ml	2715	log plain
-rw-r--r--	nativelibrary.mli	767	log plain
-rw-r--r--	nativevalues.ml	15598	log plain
-rw-r--r--	nativevalues.mli	4907	log plain
-rw-r--r--	opaqueproof.ml	5896	log plain
-rw-r--r--	opaqueproof.mli	3313	log plain
-rw-r--r--	pre_env.ml	5742	log plain
-rw-r--r--	pre_env.mli	3068	log plain
-rw-r--r--	reduction.ml	36926	log plain
-rw-r--r--	reduction.mli	5033	log plain
-rw-r--r--	retroknowledge.ml	7476	log plain
-rw-r--r--	retroknowledge.mli	6858	log plain
-rw-r--r--	safe_typing.ml	33949	log plain
-rw-r--r--	safe_typing.mli	7637	log plain
-rw-r--r--	sorts.ml	2643	log plain
-rw-r--r--	sorts.mli	1204	log plain
-rw-r--r--	subtyping.ml	18057	log plain
-rw-r--r--	subtyping.mli	648	log plain
-rw-r--r--	term.ml	19990	log plain
-rw-r--r--	term.mli	22443	log plain
-rw-r--r--	term_typing.ml	24075	log plain
-rw-r--r--	term_typing.mli	2938	log plain
-rw-r--r--	type_errors.ml	4643	log plain
-rw-r--r--	type_errors.mli	4207	log plain
-rw-r--r--	typeops.ml	17130	log plain
-rw-r--r--	typeops.mli	3748	log plain
-rw-r--r--	uGraph.ml	28867	log plain
-rw-r--r--	uGraph.mli	2343	log plain
-rw-r--r--	uint31.ml	4093	log plain
-rw-r--r--	uint31.mli	912	log plain
-rw-r--r--	univ.ml	33826	log plain
-rw-r--r--	univ.mli	15469	log plain
-rw-r--r--	vars.ml	11107	log plain
-rw-r--r--	vars.mli	6837	log plain
-rw-r--r--	vconv.ml	7555	log plain
-rw-r--r--	vconv.mli	983	log plain
-rw-r--r--	vm.ml	22344	log plain
-rw-r--r--	vm.mli	2873	log plain