kernel - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	.merlin.in	109	log plain
d---------	byterun	519	log plain
-rw-r--r--	cClosure.ml	36988	log plain
-rw-r--r--	cClosure.mli	7333	log plain
-rw-r--r--	cPrimitives.ml	2181	log plain
-rw-r--r--	cPrimitives.mli	1088	log plain
-rw-r--r--	cbytecodes.ml	9598	log plain
-rw-r--r--	cbytecodes.mli	6335	log plain
-rw-r--r--	cbytegen.ml	35690	log plain
-rw-r--r--	cbytegen.mli	1280	log plain
-rw-r--r--	cemitcodes.ml	15893	log plain
-rw-r--r--	cemitcodes.mli	858	log plain
-rw-r--r--	cinstr.mli	2183	log plain
-rw-r--r--	clambda.ml	27727	log plain
-rw-r--r--	clambda.mli	1227	log plain
-rw-r--r--	constr.ml	53952	log plain
-rw-r--r--	constr.mli	25145	log plain
-rw-r--r--	context.ml	17384	log plain
-rw-r--r--	context.mli	12423	log plain
-rw-r--r--	conv_oracle.ml	3773	log plain
-rw-r--r--	conv_oracle.mli	1856	log plain
-rw-r--r--	cooking.ml	8585	log plain
-rw-r--r--	cooking.mli	1299	log plain
-rw-r--r--	csymtable.ml	6136	log plain
-rw-r--r--	csymtable.mli	923	log plain
-rw-r--r--	declarations.ml	11718	log plain
-rw-r--r--	declareops.ml	13468	log plain
-rw-r--r--	declareops.mli	3005	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	dune	521	log plain
-rw-r--r--	entries.ml	4559	log plain
-rw-r--r--	environ.ml	23963	log plain
-rw-r--r--	environ.mli	12696	log plain
-rw-r--r--	esubst.ml	6859	log plain
-rw-r--r--	esubst.mli	3437	log plain
-rw-r--r--	evar.ml	877	log plain
-rw-r--r--	evar.mli	1526	log plain
-rw-r--r--	indtypes.ml	40123	log plain
-rw-r--r--	indtypes.mli	2037	log plain
-rw-r--r--	inductive.ml	46735	log plain
-rw-r--r--	inductive.mli	5410	log plain
-rw-r--r--	kernel.mllib	452	log plain
-rw-r--r--	make-opcodes	170	log plain
-rwxr-xr-x	make_opcodes.sh	162	log plain
-rw-r--r--	mod_subst.ml	17739	log plain
-rw-r--r--	mod_subst.mli	5881	log plain
-rw-r--r--	mod_typing.ml	14309	log plain
-rw-r--r--	mod_typing.mli	2373	log plain
-rw-r--r--	modops.ml	22812	log plain
-rw-r--r--	modops.mli	5145	log plain
-rw-r--r--	names.ml	30599	log plain
-rw-r--r--	names.mli	18034	log plain
-rw-r--r--	nativecode.ml	75788	log plain
-rw-r--r--	nativecode.mli	2517	log plain
-rw-r--r--	nativeconv.ml	7183	log plain
-rw-r--r--	nativeconv.mli	1053	log plain
-rw-r--r--	nativeinstr.mli	2665	log plain
-rw-r--r--	nativelambda.ml	21971	log plain
-rw-r--r--	nativelambda.mli	1656	log plain
-rw-r--r--	nativelib.ml	5784	log plain
-rw-r--r--	nativelib.mli	1381	log plain
-rw-r--r--	nativelibrary.ml	2828	log plain
-rw-r--r--	nativelibrary.mli	917	log plain
-rw-r--r--	nativevalues.ml	15443	log plain
-rw-r--r--	nativevalues.mli	5059	log plain
-rw-r--r--	opaqueproof.ml	6061	log plain
-rw-r--r--	opaqueproof.mli	3457	log plain
-rw-r--r--	reduction.ml	36218	log plain
-rw-r--r--	reduction.mli	5569	log plain
-rw-r--r--	retroknowledge.ml	7893	log plain
-rw-r--r--	retroknowledge.mli	6437	log plain
-rw-r--r--	safe_typing.ml	48913	log plain
-rw-r--r--	safe_typing.mli	7699	log plain
-rw-r--r--	sorts.ml	2865	log plain
-rw-r--r--	sorts.mli	1353	log plain
-rw-r--r--	subtyping.ml	15211	log plain
-rw-r--r--	subtyping.mli	799	log plain
-rw-r--r--	term.ml	13551	log plain
-rw-r--r--	term.mli	8061	log plain
-rw-r--r--	term_typing.ml	13976	log plain
-rw-r--r--	term_typing.mli	1910	log plain
-rw-r--r--	transparentState.ml	1216	log plain
-rw-r--r--	transparentState.mli	1078	log plain
-rw-r--r--	type_errors.ml	4920	log plain
-rw-r--r--	type_errors.mli	4453	log plain
-rw-r--r--	typeops.ml	19489	log plain
-rw-r--r--	typeops.mli	4610	log plain
-rw-r--r--	uGraph.ml	6118	log plain
-rw-r--r--	uGraph.mli	3437	log plain
-rw-r--r--	uint31.ml	4093	log plain
-rw-r--r--	uint31.mli	912	log plain
-rw-r--r--	univ.ml	35289	log plain
-rw-r--r--	univ.mli	16073	log plain
-rw-r--r--	vars.ml	10243	log plain
-rw-r--r--	vars.mli	6890	log plain
-rw-r--r--	vconv.ml	7873	log plain
-rw-r--r--	vconv.mli	1032	log plain
-rw-r--r--	vm.ml	5961	log plain
-rw-r--r--	vm.mli	1446	log plain
-rw-r--r--	vmvalues.ml	22971	log plain
-rw-r--r--	vmvalues.mli	4875	log plain