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

Mode	Name	Size
-rw-r--r--	.cvsignore	1	log plain
-rw-r--r--	Abstract.v	446	log plain
-rw-r--r--	Case1.v	335	log plain
-rw-r--r--	Case10.v	738	log plain
-rw-r--r--	Case11.v	341	log plain
-rw-r--r--	Case12.v	1651	log plain
-rw-r--r--	Case13.v	1483	log plain
-rw-r--r--	Case14.v	510	log plain
-rw-r--r--	Case15.v	1318	log plain
-rw-r--r--	Case16.v	405	log plain
-rw-r--r--	Case17.v	1850	log plain
-rw-r--r--	Case2.v	306	log plain
-rw-r--r--	Case5.v	365	log plain
-rw-r--r--	Case6.v	583	log plain
-rw-r--r--	Case7.v	474	log plain
-rw-r--r--	Case8.v	338	log plain
-rw-r--r--	Case9.v	2237	log plain
-rw-r--r--	CaseAlias.v	386	log plain
-rw-r--r--	Cases.v	38183	log plain
-rw-r--r--	CasesDep.v	10927	log plain
-rw-r--r--	Check.v	795	log plain
-rw-r--r--	Conjecture.v	231	log plain
-rw-r--r--	DHyp.v	1	log plain
-rw-r--r--	Decompose.v	218	log plain
-rw-r--r--	Destruct.v	243	log plain
-rw-r--r--	DiscrR.v	435	log plain
-rw-r--r--	Discriminate.v	206	log plain
-rw-r--r--	Field.v	1654	log plain
-rw-r--r--	Fixpoint.v	981	log plain
-rw-r--r--	Fourier.v	283	log plain
-rw-r--r--	Funind.v	9076	log plain
-rw-r--r--	Generalize.v	176	log plain
-rw-r--r--	Hints.v	1261	log plain
-rw-r--r--	If.v	202	log plain
-rw-r--r--	ImplicitTactic.v	549	log plain
-rw-r--r--	Inductive.v	1239	log plain
-rw-r--r--	Injection.v	928	log plain
-rw-r--r--	Inversion.v	2676	log plain
-rw-r--r--	LetIn.v	356	log plain
-rw-r--r--	MatchFail.v	822	log plain
-rw-r--r--	Mod_ltac.v	302	log plain
-rw-r--r--	Mod_params.v	1445	log plain
-rw-r--r--	Mod_strengthen.v	963	log plain
-rw-r--r--	Mod_type.v	269	log plain
-rw-r--r--	NatRing.v	133	log plain
-rw-r--r--	Omega.v	1907	log plain
-rw-r--r--	Omega2.v	764	log plain
-rw-r--r--	PPFix.v	207	log plain
-rw-r--r--	Print.v	282	log plain
-rw-r--r--	Projection.v	1154	log plain
-rw-r--r--	RecTutorial.v	25210	log plain
-rw-r--r--	Record.v	106	log plain
-rw-r--r--	Reg.v	3094	log plain
-rw-r--r--	Remark.v	172	log plain
-rw-r--r--	Rename.v	86	log plain
-rw-r--r--	Require.v	88	log plain
-rw-r--r--	Reset.v	77	log plain
-rw-r--r--	Scopes.v	157	log plain
-rw-r--r--	Simplify_eq.v	258	log plain
-rw-r--r--	Tauto.v	5157	log plain
-rw-r--r--	TestRefine.v	4407	log plain
-rw-r--r--	Try.v	182	log plain
-rw-r--r--	autorewritein.v	527	log plain
-rw-r--r--	cc.v	1759	log plain
-rw-r--r--	coercions.v	724	log plain
-rw-r--r--	coqbugs0181.v	211	log plain
-rw-r--r--	destruct.v	237	log plain
-rw-r--r--	eauto.v	1868	log plain
-rw-r--r--	eqdecide.v	912	log plain
-rw-r--r--	evars.v	1660	log plain
-rw-r--r--	extraction.v	112	log plain
-rw-r--r--	fix.v	1732	log plain
-rw-r--r--	if.v	164	log plain
-rw-r--r--	implicit.v	786	log plain
-rw-r--r--	import_lib.v	3467	log plain
-rw-r--r--	import_mod.v	993	log plain
-rw-r--r--	inds_type_sec.v	594	log plain
-rw-r--r--	induct.v	698	log plain
-rw-r--r--	intros.v	168	log plain
-rw-r--r--	ltac.v	2975	log plain
-rw-r--r--	mutual_ind.v	1604	log plain
-rw-r--r--	options.v	686	log plain
-rw-r--r--	params_ind.v	93	log plain
-rw-r--r--	refine.v	1345	log plain
-rw-r--r--	rewrite.v	530	log plain
-rw-r--r--	set.v	90	log plain
-rw-r--r--	setoid_test.v	1953	log plain
-rw-r--r--	setoid_test2.v	8151	log plain
-rw-r--r--	setoid_test_function_space.v	1387	log plain
-rw-r--r--	simpl.v	655	log plain
-rw-r--r--	unfold.v	644	log plain
-rw-r--r--	univers.v	1646	log plain