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	33079	log plain
-rw-r--r--	cbytegen.mli	1742	log plain
-rw-r--r--	cemitcodes.ml	11963	log plain
-rw-r--r--	cemitcodes.mli	1013	log plain
-rw-r--r--	closure.ml	34699	log plain
-rw-r--r--	closure.mli	6562	log plain
-rw-r--r--	constr.ml	27821	log plain
-rw-r--r--	constr.mli	8613	log plain
-rw-r--r--	context.ml	4474	log plain
-rw-r--r--	context.mli	4236	log plain
-rw-r--r--	conv_oracle.ml	2523	log plain
-rw-r--r--	conv_oracle.mli	1500	log plain
-rw-r--r--	cooking.ml	5578	log plain
-rw-r--r--	cooking.mli	1048	log plain
-rw-r--r--	csymtable.ml	7232	log plain
-rw-r--r--	csymtable.mli	708	log plain
-rw-r--r--	declarations.mli	8037	log plain
-rw-r--r--	declareops.ml	8823	log plain
-rw-r--r--	declareops.mli	2621	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	entries.mli	2913	log plain
-rw-r--r--	environ.ml	18599	log plain
-rw-r--r--	environ.mli	8378	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--	indtypes.ml	26139	log plain
-rw-r--r--	indtypes.mli	1382	log plain
-rw-r--r--	inductive.ml	35577	log plain
-rw-r--r--	inductive.mli	4472	log plain
-rw-r--r--	kernel.mllib	379	log plain
-rw-r--r--	make-opcodes	102	log plain
-rw-r--r--	mod_subst.ml	17193	log plain
-rw-r--r--	mod_subst.mli	5452	log plain
-rw-r--r--	mod_typing.ml	11880	log plain
-rw-r--r--	mod_typing.mli	1915	log plain
-rw-r--r--	modops.ml	21334	log plain
-rw-r--r--	modops.mli	4815	log plain
-rw-r--r--	names.ml	21052	log plain
-rw-r--r--	names.mli	19191	log plain
-rw-r--r--	nativecode.ml	61388	log plain
-rw-r--r--	nativecode.mli	2235	log plain
-rw-r--r--	nativeconv.ml	5419	log plain
-rw-r--r--	nativeconv.mli	711	log plain
-rw-r--r--	nativelambda.ml	22188	log plain
-rw-r--r--	nativelambda.mli	2392	log plain
-rw-r--r--	nativelib.ml	3704	log plain
-rw-r--r--	nativelib.mli	1135	log plain
-rw-r--r--	nativelibrary.ml	2276	log plain
-rw-r--r--	nativelibrary.mli	854	log plain
-rw-r--r--	nativevalues.ml	7582	log plain
-rw-r--r--	nativevalues.mli	2951	log plain
-rw-r--r--	opaqueproof.ml	4321	log plain
-rw-r--r--	opaqueproof.mli	3031	log plain
-rw-r--r--	pre_env.ml	4844	log plain
-rw-r--r--	pre_env.mli	2584	log plain
-rw-r--r--	reduction.ml	21714	log plain
-rw-r--r--	reduction.mli	3570	log plain
-rw-r--r--	retroknowledge.ml	8666	log plain
-rw-r--r--	retroknowledge.mli	5927	log plain
-rw-r--r--	safe_typing.ml	27018	log plain
-rw-r--r--	safe_typing.mli	5035	log plain
-rw-r--r--	sorts.ml	2024	log plain
-rw-r--r--	sorts.mli	1073	log plain
-rw-r--r--	subtyping.ml	16766	log plain
-rw-r--r--	subtyping.mli	650	log plain
-rw-r--r--	term.ml	20929	log plain
-rw-r--r--	term.mli	14748	log plain
-rw-r--r--	term_typing.ml	9017	log plain
-rw-r--r--	term_typing.mli	1580	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	16418	log plain
-rw-r--r--	typeops.mli	3713	log plain
-rw-r--r--	univ.ml	35618	log plain
-rw-r--r--	univ.mli	5448	log plain
-rw-r--r--	vars.ml	6794	log plain
-rw-r--r--	vars.mli	2967	log plain
-rw-r--r--	vconv.ml	8076	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