proofs - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	clenv.ml	17336	log plain
-rw-r--r--	clenv.mli	5514	log plain
-rw-r--r--	clenvtac.ml	3825	log plain
-rw-r--r--	clenvtac.mli	1178	log plain
-rw-r--r--	doc.tex	424	log plain
-rw-r--r--	evar_refiner.ml	2204	log plain
-rw-r--r--	evar_refiner.mli	950	log plain
-rw-r--r--	goal.ml	20495	log plain
-rw-r--r--	goal.mli	8820	log plain
-rw-r--r--	logic.ml	25810	log plain
-rw-r--r--	logic.mli	1851	log plain
-rw-r--r--	pfedit.ml	4720	log plain
-rw-r--r--	pfedit.mli	6159	log plain
-rw-r--r--	proof.ml	9944	log plain
-rw-r--r--	proof.mli	5153	log plain
-rw-r--r--	proof_global.ml	9656	log plain
-rw-r--r--	proof_global.mli	3688	log plain
-rw-r--r--	proof_type.ml	2740	log plain
-rw-r--r--	proof_type.mli	4526	log plain
-rw-r--r--	proofs.mllib	131	log plain
-rw-r--r--	proofview.ml	19065	log plain
-rw-r--r--	proofview.mli	9324	log plain
-rw-r--r--	redexpr.ml	7756	log plain
-rw-r--r--	redexpr.mli	1657	log plain
-rw-r--r--	refiner.ml	14219	log plain
-rw-r--r--	refiner.mli	7370	log plain
-rw-r--r--	tacexpr.ml	13206	log plain
-rw-r--r--	tacmach.ml	7217	log plain
-rw-r--r--	tacmach.mli	5822	log plain
-rw-r--r--	tactic_debug.ml	6447	log plain
-rw-r--r--	tactic_debug.mli	2779	log plain
-rw-r--r--	tmp-src	1852	log plain