kernel - coq - the Coq proof assistant

Mode	Name	Size
d---------	byterun	444	log plain
-rw-r--r--	cClosure.ml	37148	log plain
-rw-r--r--	cClosure.mli	7929	log plain
-rw-r--r--	cbytecodes.ml	11023	log plain
-rw-r--r--	cbytecodes.mli	7393	log plain
-rw-r--r--	cbytegen.ml	42448	log plain
-rw-r--r--	cbytegen.mli	1922	log plain
-rw-r--r--	cemitcodes.ml	13440	log plain
-rw-r--r--	cemitcodes.mli	988	log plain
-rw-r--r--	constr.ml	38472	log plain
-rw-r--r--	constr.mli	15239	log plain
-rw-r--r--	context.ml	17121	log plain
-rw-r--r--	context.mli	12024	log plain
-rw-r--r--	conv_oracle.ml	3230	log plain
-rw-r--r--	conv_oracle.mli	1697	log plain
-rw-r--r--	cooking.ml	8691	log plain
-rw-r--r--	cooking.mli	1093	log plain
-rw-r--r--	csymtable.ml	7353	log plain
-rw-r--r--	csymtable.mli	708	log plain
-rw-r--r--	declarations.mli	10757	log plain
-rw-r--r--	declareops.ml	13471	log plain
-rw-r--r--	declareops.mli	2895	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	entries.mli	4014	log plain
-rw-r--r--	environ.ml	22731	log plain
-rw-r--r--	environ.mli	10522	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	38147	log plain
-rw-r--r--	indtypes.mli	1726	log plain
-rw-r--r--	inductive.ml	46099	log plain
-rw-r--r--	inductive.mli	5290	log plain
-rw-r--r--	kernel.mllib	404	log plain
-rw-r--r--	make-opcodes	170	log plain
-rw-r--r--	mod_subst.ml	18051	log plain
-rw-r--r--	mod_subst.mli	5939	log plain
-rw-r--r--	mod_typing.ml	14815	log plain
-rw-r--r--	mod_typing.mli	2235	log plain
-rw-r--r--	modops.ml	21911	log plain
-rw-r--r--	modops.mli	5008	log plain
-rw-r--r--	names.ml	27142	log plain
-rw-r--r--	names.mli	23390	log plain
-rw-r--r--	nativecode.ml	73939	log plain
-rw-r--r--	nativecode.mli	2319	log plain
-rw-r--r--	nativeconv.ml	6736	log plain
-rw-r--r--	nativeconv.mli	901	log plain
-rw-r--r--	nativeinstr.mli	2211	log plain
-rw-r--r--	nativelambda.ml	21655	log plain
-rw-r--r--	nativelambda.mli	1550	log plain
-rw-r--r--	nativelib.ml	5396	log plain
-rw-r--r--	nativelib.mli	1214	log plain
-rw-r--r--	nativelibrary.ml	2709	log plain
-rw-r--r--	nativelibrary.mli	768	log plain
-rw-r--r--	nativevalues.ml	15574	log plain
-rw-r--r--	nativevalues.mli	4903	log plain
-rw-r--r--	opaqueproof.ml	5943	log plain
-rw-r--r--	opaqueproof.mli	3360	log plain
-rw-r--r--	pre_env.ml	5735	log plain
-rw-r--r--	pre_env.mli	3078	log plain
-rw-r--r--	primitives.ml	2031	log plain
-rw-r--r--	primitives.mli	938	log plain
-rw-r--r--	reduction.ml	29879	log plain
-rw-r--r--	reduction.mli	4758	log plain
-rw-r--r--	retroknowledge.ml	7464	log plain
-rw-r--r--	retroknowledge.mli	6866	log plain
-rw-r--r--	safe_typing.ml	33185	log plain
-rw-r--r--	safe_typing.mli	7407	log plain
-rw-r--r--	sorts.ml	2637	log plain
-rw-r--r--	sorts.mli	1198	log plain
-rw-r--r--	subtyping.ml	19731	log plain
-rw-r--r--	subtyping.mli	650	log plain
-rw-r--r--	term.ml	23148	log plain
-rw-r--r--	term.mli	17028	log plain
-rw-r--r--	term_typing.ml	22634	log plain
-rw-r--r--	term_typing.mli	3140	log plain
-rw-r--r--	type_errors.ml	4627	log plain
-rw-r--r--	type_errors.mli	4217	log plain
-rw-r--r--	typeops.ml	19194	log plain
-rw-r--r--	typeops.mli	4029	log plain
-rw-r--r--	uGraph.ml	28400	log plain
-rw-r--r--	uGraph.mli	2249	log plain
-rw-r--r--	uint31.ml	4093	log plain
-rw-r--r--	uint31.mli	912	log plain
-rw-r--r--	univ.ml	33812	log plain
-rw-r--r--	univ.mli	12860	log plain
-rw-r--r--	vars.ml	11168	log plain
-rw-r--r--	vars.mli	6849	log plain
-rw-r--r--	vconv.ml	7279	log plain
-rw-r--r--	vconv.mli	981	log plain
-rw-r--r--	vm.ml	22313	log plain
-rw-r--r--	vm.mli	2380	log plain