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

Mode	Name	Size
-rw-r--r--	Abstract.v	446	log plain
-rw-r--r--	AdvancedCanonicalStructure.v	2979	log plain
-rw-r--r--	AdvancedTypeClasses.v	2229	log plain
-rw-r--r--	CanonicalStructure.v	713	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	2074	log plain
-rw-r--r--	Case13.v	2149	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--	Case18.v	513	log plain
-rw-r--r--	Case19.v	272	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-bug1834.v	379	log plain
-rw-r--r--	Cases.v	38278	log plain
-rw-r--r--	CasesDep.v	12108	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--	DiscrR.v	435	log plain
-rw-r--r--	Discriminate.v	571	log plain
-rw-r--r--	Equations.v	10700	log plain
-rw-r--r--	Field.v	1863	log plain
-rw-r--r--	Fixpoint.v	1400	log plain
-rw-r--r--	Fourier.v	283	log plain
-rw-r--r--	Funind.v	10176	log plain
-rw-r--r--	Generalization.v	253	log plain
-rw-r--r--	Generalize.v	176	log plain
-rw-r--r--	Hints.v	1261	log plain
-rw-r--r--	ImplicitArguments.v	545	log plain
-rw-r--r--	ImplicitTactic.v	549	log plain
-rw-r--r--	Inductive.v	1427	log plain
-rw-r--r--	Injection.v	1769	log plain
-rw-r--r--	Inversion.v	2859	log plain
-rw-r--r--	LegacyField.v	1768	log plain
-rw-r--r--	LetIn.v	356	log plain
-rw-r--r--	LetPat.v	1756	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	125	log plain
-rw-r--r--	Notations.v	1171	log plain
-rw-r--r--	Omega.v	2197	log plain
-rw-r--r--	Omega0.v	2449	log plain
-rw-r--r--	Omega2.v	764	log plain
-rw-r--r--	OmegaPre.v	2183	log plain
-rw-r--r--	PPFix.v	207	log plain
-rw-r--r--	Print.v	282	log plain
-rw-r--r--	ProgramWf.v	2035	log plain
-rw-r--r--	Projection.v	1154	log plain
-rw-r--r--	ROmega.v	2243	log plain
-rw-r--r--	ROmega0.v	2564	log plain
-rw-r--r--	ROmega2.v	984	log plain
-rw-r--r--	ROmegaPre.v	2204	log plain
-rw-r--r--	RecTutorial.v	25255	log plain
-rw-r--r--	Record.v	2253	log plain
-rw-r--r--	Reg.v	3094	log plain
-rw-r--r--	Remark.v	172	log plain
-rw-r--r--	Rename.v	220	log plain
-rw-r--r--	Reordering.v	378	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	4319	log plain
-rw-r--r--	Try.v	182	log plain
-rw-r--r--	apply.v	6956	log plain
-rw-r--r--	autorewritein.v	521	log plain
-rw-r--r--	cc.v	2403	log plain
-rw-r--r--	change.v	186	log plain
-rw-r--r--	clear.v	291	log plain
-rw-r--r--	coercions.v	2133	log plain
-rw-r--r--	conv_pbs.v	7485	log plain
-rw-r--r--	coqbugs0181.v	211	log plain
-rw-r--r--	decl_mode.v	5547	log plain
-rw-r--r--	dependentind.v	3331	log plain
-rw-r--r--	destruct.v	1219	log plain
-rw-r--r--	eauto.v	1868	log plain
-rw-r--r--	eqdecide.v	912	log plain
-rw-r--r--	evars.v	6739	log plain
-rw-r--r--	extraction.v	14264	log plain
-rw-r--r--	fix.v	2212	log plain
-rw-r--r--	guard.v	322	log plain
-rw-r--r--	hyps_inclusion.v	1153	log plain
-rw-r--r--	if.v	366	log plain
-rw-r--r--	implicit.v	1117	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--	instantiate.v	292	log plain
-rw-r--r--	intros.v	168	log plain
-rw-r--r--	ltac.v	4558	log plain
-rw-r--r--	mutual_ind.v	1604	log plain
-rw-r--r--	options.v	690	log plain
-rw-r--r--	params_ind.v	93	log plain
-rw-r--r--	parsing.v	243	log plain
-rw-r--r--	pattern.v	1261	log plain
-rw-r--r--	polymorphism.v	220	log plain
-rw-r--r--	refine.v	2668	log plain
-rw-r--r--	replace.v	359	log plain
-rw-r--r--	rewrite.v	944	log plain
-rw-r--r--	rewrite_in.v	148	log plain
-rw-r--r--	rewrite_iterated.v	545	log plain
-rw-r--r--	set.v	90	log plain
-rw-r--r--	setoid_ring_module.v	925	log plain
-rw-r--r--	setoid_test.v	2657	log plain
-rw-r--r--	setoid_test2.v	8257	log plain
-rw-r--r--	setoid_test_function_space.v	1434	log plain
-rw-r--r--	simpl.v	1239	log plain
-rw-r--r--	specialize.v	1459	log plain
-rw-r--r--	unfold.v	644	log plain
-rw-r--r--	unicode_utf8.v	2172	log plain
-rw-r--r--	unification.v	3912	log plain
-rw-r--r--	univers.v	1752	log plain