correctness « contrib - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	.cvsignore	12	log plain
-rw-r--r--	Arrays.v	2530	log plain
-rw-r--r--	Arrays_stuff.v	675	log plain
-rw-r--r--	Correctness.v	1018	log plain
-rw-r--r--	Exchange.v	2865	log plain
-rw-r--r--	MakeProgramsState.v	71	log plain
-rw-r--r--	Permut.v	5437	log plain
-rw-r--r--	ProgBool.v	4048	log plain
-rw-r--r--	ProgInt.v	748	log plain
-rw-r--r--	ProgWf.v	2176	log plain
-rw-r--r--	ProgramsExtraction.v	1129	log plain
-rw-r--r--	Programs_stuff.v	632	log plain
-rw-r--r--	Sorted.v	5124	log plain
-rw-r--r--	Tuples.v	3349	log plain
-rw-r--r--	past.ml	3845	log plain
-rw-r--r--	past.mli	2870	log plain
-rw-r--r--	pcic.ml	5066	log plain
-rw-r--r--	pcic.mli	731	log plain
-rw-r--r--	pcicenv.ml	3323	log plain
-rw-r--r--	pcicenv.mli	1521	log plain
-rw-r--r--	pdb.ml	4944	log plain
-rw-r--r--	pdb.mli	947	log plain
-rw-r--r--	peffect.ml	3737	log plain
-rw-r--r--	peffect.mli	1215	log plain
-rw-r--r--	penv.ml	5828	log plain
-rw-r--r--	penv.mli	2750	log plain
-rw-r--r--	perror.ml	5390	log plain
-rw-r--r--	perror.mli	1656	log plain
-rw-r--r--	pextract.ml	14531	log plain
-rw-r--r--	pextract.mli	679	log plain
-rw-r--r--	pmisc.ml	4946	log plain
-rw-r--r--	pmisc.mli	2398	log plain
-rw-r--r--	pmlize.ml	10149	log plain
-rw-r--r--	pmlize.mli	766	log plain
-rw-r--r--	pmonad.ml	20865	log plain
-rw-r--r--	pmonad.mli	3486	log plain
-rw-r--r--	pred.ml	2264	log plain
-rw-r--r--	pred.mli	847	log plain
-rw-r--r--	prename.ml	3681	log plain
-rw-r--r--	prename.mli	1981	log plain
-rw-r--r--	preuves.v	1554	log plain
-rw-r--r--	psyntax.ml4	16732	log plain
-rw-r--r--	psyntax.mli	864	log plain
-rw-r--r--	ptactic.ml	8665	log plain
-rw-r--r--	ptactic.mli	1029	log plain
-rw-r--r--	ptype.ml	2254	log plain
-rw-r--r--	ptype.mli	1430	log plain
-rw-r--r--	ptyping.ml	19212	log plain
-rw-r--r--	ptyping.mli	1260	log plain
-rw-r--r--	putil.ml	8832	log plain
-rw-r--r--	putil.mli	2596	log plain
-rw-r--r--	pwp.ml	10875	log plain
-rw-r--r--	pwp.mli	756	log plain