success « test-suite - coq - the Coq proof assistant

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--	Case13.v	959	log plain
-rw-r--r--	Case14.v	489	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--	CaseAlias.v	380	log plain
-rw-r--r--	Cases.v	46153	log plain
-rw-r--r--	CasesDep.v	10699	log plain
-rw-r--r--	Check.v	788	log plain
-rw-r--r--	DHyp.v	205	log plain
-rw-r--r--	Decompose.v	187	log plain
-rw-r--r--	Destruct.v	195	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	1559	log plain
-rw-r--r--	Injection.v	254	log plain
-rw-r--r--	LetIn.v	314	log plain
-rw-r--r--	MatchFail.v	958	log plain
-rw-r--r--	NatRing.v	144	log plain
-rw-r--r--	Omega.v	982	log plain
-rw-r--r--	Print.v	297	log plain
-rw-r--r--	Reg.v	2266	log plain
-rw-r--r--	Remark.v	122	log plain
-rw-r--r--	Rename.v	78	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--	coercions.v	202	log plain
-rw-r--r--	eauto.v	1262	log plain
-rw-r--r--	eqdecide.v	831	log plain
-rw-r--r--	evars.v	1319	log plain
-rw-r--r--	fix.v	1654	log plain
-rw-r--r--	if.v	154	log plain
-rw-r--r--	implicit.v	434	log plain
-rw-r--r--	inds_type_sec.v	582	log plain
-rw-r--r--	induct.v	686	log plain
-rw-r--r--	ltac.v	329	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
-rw-r--r--	univers.v	273	log plain