success « test-suite - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	Case1.v	400	log plain
-rw-r--r--	Case10.v	764	log plain
-rw-r--r--	Case11.v	285	log plain
-rw-r--r--	Case12.v	1442	log plain
-rw-r--r--	Case2.v	339	log plain
-rw-r--r--	Case5.v	351	log plain
-rw-r--r--	Case6.v	597	log plain
-rw-r--r--	Case7.v	459	log plain
-rw-r--r--	Case9.v	2270	log plain
-rw-r--r--	Cases.v	46378	log plain
-rw-r--r--	CasesDep.v	10139	log plain
-rw-r--r--	Check.v	788	log plain
-rw-r--r--	Decompose.v	187	log plain
-rw-r--r--	DiscrR.v	395	log plain
-rw-r--r--	Discriminate.v	196	log plain
-rw-r--r--	Field.v	1437	log plain
-rw-r--r--	Fourier.v	301	log plain
-rw-r--r--	Hints.v	1541	log plain
-rw-r--r--	Injection.v	254	log plain
-rw-r--r--	LetIn.v	314	log plain
-rw-r--r--	Remark.v	122	log plain
-rw-r--r--	Require.v	85	log plain
-rw-r--r--	Simplify_eq.v	241	log plain
-rw-r--r--	Tauto.v	4413	log plain
-rw-r--r--	eauto.v	1262	log plain
-rw-r--r--	eqdecide.v	831	log plain
-rw-r--r--	evars.v	698	log plain
-rw-r--r--	fix.v	1654	log plain
-rw-r--r--	if.v	153	log plain
-rw-r--r--	inds_type_sec.v	582	log plain
-rw-r--r--	induct.v	686	log plain
-rw-r--r--	mutual_ind.v	1508	log plain
-rw-r--r--	options.v	662	log plain
-rw-r--r--	refine.v	282	log plain
-rw-r--r--	setoid_test.v	1708	log plain
-rw-r--r--	unfold.v	641	log plain