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

Mode	Name	Size
-rw-r--r--	.cvsignore	1	log plain
-rw-r--r--	Abstract.v8	445	log plain
-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--	Case15.v	1303	log plain
-rw-r--r--	Case16.v	388	log plain
-rw-r--r--	Case17.v	1893	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--	Case8.v	280	log plain
-rw-r--r--	Case9.v	2270	log plain
-rw-r--r--	CaseAlias.v	380	log plain
-rw-r--r--	Cases.v	46156	log plain
-rw-r--r--	CasesDep.v	10886	log plain
-rw-r--r--	Check.v	795	log plain
-rw-r--r--	Conjecture.v	210	log plain
-rw-r--r--	DHyp.v	217	log plain
-rw-r--r--	Decompose.v	187	log plain
-rw-r--r--	Destruct.v	236	log plain
-rw-r--r--	DiscrR.v	395	log plain
-rw-r--r--	Discriminate.v	196	log plain
-rw-r--r--	Field.v	1444	log plain
-rw-r--r--	Fixpoint.v8	980	log plain
-rw-r--r--	Fourier.v	300	log plain
-rw-r--r--	Funind.v	9863	log plain
-rw-r--r--	Generalize.v	137	log plain
-rw-r--r--	Hints.v	1559	log plain
-rw-r--r--	If.v8	201	log plain
-rw-r--r--	ImplicitTactic.v8	548	log plain
-rw-r--r--	Inductive.v	1057	log plain
-rw-r--r--	Injection.v	814	log plain
-rw-r--r--	Inversion.v	2590	log plain
-rw-r--r--	LetIn.v	314	log plain
-rw-r--r--	MatchFail.v	958	log plain
-rw-r--r--	Mod_ltac.v	264	log plain
-rw-r--r--	Mod_params.v	1325	log plain
-rw-r--r--	Mod_strengthen.v8	962	log plain
-rw-r--r--	NatRing.v	144	log plain
-rw-r--r--	Omega.v	1702	log plain
-rw-r--r--	Omega2.v8	763	log plain
-rw-r--r--	PPFix.v8	206	log plain
-rw-r--r--	Print.v	297	log plain
-rw-r--r--	Projection.v	1059	log plain
-rw-r--r--	RecTutorial.v8	25209	log plain
-rw-r--r--	Record.v	105	log plain
-rw-r--r--	Reg.v	2837	log plain
-rw-r--r--	Remark.v	172	log plain
-rw-r--r--	Rename.v	78	log plain
-rw-r--r--	Require.v	85	log plain
-rw-r--r--	Reset.v	75	log plain
-rw-r--r--	Scopes.v	157	log plain
-rw-r--r--	Simplify_eq.v	241	log plain
-rw-r--r--	Tauto.v	4777	log plain
-rw-r--r--	TestRefine.v	4058	log plain
-rw-r--r--	Try.v	176	log plain
-rw-r--r--	autorewritein.v8	526	log plain
-rw-r--r--	cc.v	1519	log plain
-rw-r--r--	coercions.v	710	log plain
-rw-r--r--	coqbugs0181.v	202	log plain
-rw-r--r--	destruct.v	227	log plain
-rw-r--r--	eauto.v	1706	log plain
-rw-r--r--	eqdecide.v	838	log plain
-rw-r--r--	evars.v	1519	log plain
-rw-r--r--	fix.v	1661	log plain
-rw-r--r--	if.v	154	log plain
-rw-r--r--	implicit.v	741	log plain
-rw-r--r--	import_lib.v	3550	log plain
-rw-r--r--	import_mod.v	981	log plain
-rw-r--r--	inds_type_sec.v	590	log plain
-rw-r--r--	induct.v	693	log plain
-rw-r--r--	intros.v8	167	log plain
-rw-r--r--	ltac.v	2850	log plain
-rw-r--r--	mutual_ind.v	1515	log plain
-rw-r--r--	options.v	662	log plain
-rw-r--r--	params_ind.v	90	log plain
-rw-r--r--	refine.v	1200	log plain
-rw-r--r--	rewrite.v	540	log plain
-rw-r--r--	set.v8	89	log plain
-rw-r--r--	setoid_test.v8	1952	log plain
-rw-r--r--	setoid_test2.v8	8150	log plain
-rw-r--r--	setoid_test_function_space.v8	1386	log plain
-rw-r--r--	simpl.v8	654	log plain
-rw-r--r--	unfold.v	648	log plain
-rw-r--r--	univers.v	1569	log plain