kernel - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	.merlin.in	109	log plain
d---------	byterun	611	log plain
-rw-r--r--	cClosure.ml	45107	log plain
-rw-r--r--	cClosure.mli	7775	log plain
-rw-r--r--	cPrimitives.ml	3853	log plain
-rw-r--r--	cPrimitives.mli	1679	log plain
-rw-r--r--	cbytecodes.ml	5200	log plain
-rw-r--r--	cbytecodes.mli	3059	log plain
-rw-r--r--	cbytegen.ml	32887	log plain
-rw-r--r--	cbytegen.mli	1308	log plain
-rw-r--r--	cemitcodes.ml	16485	log plain
-rw-r--r--	cemitcodes.mli	1383	log plain
-rw-r--r--	clambda.ml	25604	log plain
-rw-r--r--	clambda.mli	1407	log plain
-rw-r--r--	constr.ml	54495	log plain
-rw-r--r--	constr.mli	25239	log plain
-rw-r--r--	context.ml	17630	log plain
-rw-r--r--	context.mli	12548	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	8688	log plain
-rw-r--r--	cooking.mli	1328	log plain
-rw-r--r--	csymtable.ml	6136	log plain
-rw-r--r--	csymtable.mli	923	log plain
-rw-r--r--	declarations.ml	11826	log plain
-rw-r--r--	declareops.ml	13542	log plain
-rw-r--r--	declareops.mli	3005	log plain
-rw-r--r--	doc.tex	277	log plain
-rw-r--r--	dune	745	log plain
-rw-r--r--	entries.ml	4771	log plain
-rw-r--r--	environ.ml	23834	log plain
-rw-r--r--	environ.mli	13280	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--	indTyping.ml	13048	log plain
-rw-r--r--	indTyping.mli	1327	log plain
-rw-r--r--	indtypes.ml	24719	log plain
-rw-r--r--	indtypes.mli	1452	log plain
-rw-r--r--	inductive.ml	46777	log plain
-rw-r--r--	inductive.mli	5410	log plain
-rw-r--r--	kernel.mllib	470	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	18197	log plain
-rw-r--r--	mod_subst.mli	5970	log plain
-rw-r--r--	mod_typing.ml	14669	log plain
-rw-r--r--	mod_typing.mli	2373	log plain
-rw-r--r--	modops.ml	22220	log plain
-rw-r--r--	modops.mli	5229	log plain
-rw-r--r--	names.ml	30648	log plain
-rw-r--r--	names.mli	19341	log plain
-rw-r--r--	nativecode.ml	74359	log plain
-rw-r--r--	nativecode.mli	2517	log plain
-rw-r--r--	nativeconv.ml	7288	log plain
-rw-r--r--	nativeconv.mli	1053	log plain
-rw-r--r--	nativelambda.ml	20834	log plain
-rw-r--r--	nativelambda.mli	2796	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	13249	log plain
-rw-r--r--	nativevalues.mli	5715	log plain
-rw-r--r--	opaqueproof.ml	6061	log plain
-rw-r--r--	opaqueproof.mli	3457	log plain
-rw-r--r--	primred.ml	6717	log plain
-rw-r--r--	primred.mli	1248	log plain
-rw-r--r--	reduction.ml	37928	log plain
-rw-r--r--	reduction.mli	5569	log plain
-rw-r--r--	retroknowledge.ml	1610	log plain
-rw-r--r--	retroknowledge.mli	1252	log plain
-rw-r--r--	safe_typing.ml	45201	log plain
-rw-r--r--	safe_typing.mli	7730	log plain
-rw-r--r--	sorts.ml	2865	log plain
-rw-r--r--	sorts.mli	1353	log plain
-rw-r--r--	subtyping.ml	15253	log plain
-rw-r--r--	subtyping.mli	799	log plain
-rw-r--r--	term.ml	13559	log plain
-rw-r--r--	term.mli	8061	log plain
-rw-r--r--	term_typing.ml	15235	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	7624	log plain
-rw-r--r--	type_errors.mli	5176	log plain
-rw-r--r--	typeops.ml	22262	log plain
-rw-r--r--	typeops.mli	4912	log plain
-rw-r--r--	uGraph.ml	6118	log plain
-rw-r--r--	uGraph.mli	3437	log plain
-rw-r--r--	uint63.mli	1095	log plain
-rw-r--r--	uint63_amd64.ml	6255	log plain
-rw-r--r--	uint63_x86.ml	7264	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	7586	log plain
-rw-r--r--	vconv.mli	1032	log plain
-rw-r--r--	vm.ml	5971	log plain
-rw-r--r--	vm.mli	1446	log plain
-rw-r--r--	vmvalues.ml	23621	log plain
-rw-r--r--	vmvalues.mli	4970	log plain
-rw-r--r--	write_uint63.ml	802	log plain