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

Mode	Name	Size
-rw-r--r--	Abstract.v	445	log plain
-rw-r--r--	AdvancedCanonicalStructure.v	3365	log plain
-rw-r--r--	AdvancedTypeClasses.v	2253	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	349	log plain
-rw-r--r--	Case12.v	2083	log plain
-rw-r--r--	Case13.v	2149	log plain
-rw-r--r--	Case14.v	510	log plain
-rw-r--r--	Case15.v	1315	log plain
-rw-r--r--	Case16.v	409	log plain
-rw-r--r--	Case17.v	1860	log plain
-rw-r--r--	Case18.v	513	log plain
-rw-r--r--	Case19.v	542	log plain
-rw-r--r--	Case2.v	306	log plain
-rw-r--r--	Case20.v	1106	log plain
-rw-r--r--	Case21.v	476	log plain
-rw-r--r--	Case22.v	1756	log plain
-rw-r--r--	Case3.v	720	log plain
-rw-r--r--	Case5.v	365	log plain
-rw-r--r--	Case6.v	583	log plain
-rw-r--r--	Case7.v	478	log plain
-rw-r--r--	Case8.v	338	log plain
-rw-r--r--	Case9.v	2269	log plain
-rw-r--r--	CaseAlias.v	2598	log plain
-rw-r--r--	CaseInClause.v	828	log plain
-rw-r--r--	Cases-bug1834.v	383	log plain
-rw-r--r--	Cases-bug3758.v	386	log plain
-rw-r--r--	Cases.v	39353	log plain
-rw-r--r--	CasesDep.v	14537	log plain
-rw-r--r--	Check.v	795	log plain
-rw-r--r--	Compat84.v	518	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	644	log plain
-rw-r--r--	Field.v	1978	log plain
-rw-r--r--	Fixpoint.v	2347	log plain
-rw-r--r--	Fourier.v	281	log plain
-rw-r--r--	Funind.v	10145	log plain
-rw-r--r--	Generalization.v	282	log plain
-rw-r--r--	Generalize.v	176	log plain
-rw-r--r--	Hints.v	2885	log plain
-rw-r--r--	ImplicitArguments.v	627	log plain
-rw-r--r--	ImplicitTactic.v	549	log plain
-rw-r--r--	Import.v	218	log plain
-rw-r--r--	Inductive.v	5058	log plain
-rw-r--r--	Injection.v	3232	log plain
-rw-r--r--	Inversion.v	5372	log plain
-rw-r--r--	LetIn.v	356	log plain
-rw-r--r--	LetPat.v	1760	log plain
-rw-r--r--	MatchFail.v	844	log plain
-rw-r--r--	Mod_ltac.v	302	log plain
-rw-r--r--	Mod_params.v	1375	log plain
-rw-r--r--	Mod_strengthen.v	963	log plain
-rw-r--r--	Mod_type.v	519	log plain
-rw-r--r--	NatRing.v	125	log plain
-rw-r--r--	Notations.v	3381	log plain
-rw-r--r--	Notations2.v	4650	log plain
-rw-r--r--	Nsatz.v	14291	log plain
-rw-r--r--	NumberScopes.v	1367	log plain
-rw-r--r--	Omega.v	2197	log plain
-rw-r--r--	Omega0.v	2427	log plain
-rw-r--r--	Omega2.v	763	log plain
-rw-r--r--	OmegaPre.v	2195	log plain
-rw-r--r--	PCase.v	1515	log plain
-rw-r--r--	PPFix.v	207	log plain
-rw-r--r--	Print.v	282	log plain
-rw-r--r--	PrintSortedUniverses.v	39	log plain
-rw-r--r--	ProgramWf.v	2278	log plain
-rw-r--r--	Projection.v	1278	log plain
-rw-r--r--	ROmega.v	2242	log plain
-rw-r--r--	ROmega0.v	2542	log plain
-rw-r--r--	ROmega2.v	982	log plain
-rw-r--r--	ROmegaPre.v	2216	log plain
-rw-r--r--	RecTutorial.v	25136	log plain
-rw-r--r--	Record.v	2399	log plain
-rw-r--r--	Reg.v	3062	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--	Scheme.v	82	log plain
-rw-r--r--	Scopes.v	454	log plain
-rw-r--r--	Section.v	136	log plain
-rw-r--r--	Simplify_eq.v	252	log plain
-rw-r--r--	TacticNotation1.v	198	log plain
-rw-r--r--	TacticNotation2.v	310	log plain
-rw-r--r--	Tauto.v	5145	log plain
-rw-r--r--	TestRefine.v	4320	log plain
-rw-r--r--	Try.v	174	log plain
-rw-r--r--	Typeclasses.v	1814	log plain
-rw-r--r--	apply.v	14153	log plain
-rw-r--r--	applyTC.v	289	log plain
-rw-r--r--	auto.v	3284	log plain
-rw-r--r--	autointros.v	462	log plain
-rw-r--r--	autorewrite.v	763	log plain
-rw-r--r--	bigQ.v	21236	log plain
-rw-r--r--	bullet.v	53	log plain
-rw-r--r--	cc.v	2878	log plain
-rw-r--r--	change.v	1592	log plain
-rw-r--r--	clear.v	290	log plain
-rw-r--r--	coercions.v	3769	log plain
-rw-r--r--	coindprim.v	1107	log plain
-rw-r--r--	conv_pbs.v	7579	log plain
-rw-r--r--	coqbugs0181.v	211	log plain
-rw-r--r--	decl_mode.v	5544	log plain
-rw-r--r--	decl_mode2.v	5234	log plain
-rw-r--r--	dependentind.v	3932	log plain
-rw-r--r--	destruct.v	9757	log plain
-rw-r--r--	eauto.v	1867	log plain
-rw-r--r--	eqdecide.v	819	log plain
-rw-r--r--	eta.v	595	log plain
-rw-r--r--	evars.v	13248	log plain
-rw-r--r--	extraction.v	14186	log plain
-rw-r--r--	extraction_dep.v	857	log plain
-rw-r--r--	extraction_impl.v	1649	log plain
-rw-r--r--	extraction_polyprop.v	362	log plain
-rw-r--r--	fix.v	2182	log plain
-rw-r--r--	guard.v	322	log plain
-rw-r--r--	hyps_inclusion.v	1160	log plain
-rw-r--r--	if.v	366	log plain
-rw-r--r--	implicit.v	2763	log plain
-rw-r--r--	import_lib.v	3415	log plain
-rw-r--r--	import_mod.v	993	log plain
-rw-r--r--	indelim.v	1359	log plain
-rw-r--r--	inds_type_sec.v	594	log plain
-rw-r--r--	induct.v	4893	log plain
-rw-r--r--	intros.v	2910	log plain
-rw-r--r--	keyedrewrite.v	1383	log plain
-rw-r--r--	letproj.v	224	log plain
-rw-r--r--	ltac.v	6617	log plain
-rw-r--r--	ltac_plus.v	356	log plain
-rw-r--r--	mutual_ind.v	1601	log plain
-rw-r--r--	namedunivs.v	2799	log plain
-rw-r--r--	options.v	690	log plain
-rw-r--r--	paralleltac.v	975	log plain
-rw-r--r--	parsing.v	218	log plain
-rw-r--r--	pattern.v	1400	log plain
-rw-r--r--	polymorphism.v	7420	log plain
-rw-r--r--	primitiveproj.v	4481	log plain
-rw-r--r--	proof_using.v	2575	log plain
-rw-r--r--	qed_export.v	323	log plain
-rw-r--r--	record_syntax.v	802	log plain
-rw-r--r--	refine.v	2672	log plain
-rw-r--r--	remember.v	626	log plain
-rw-r--r--	replace.v	635	log plain
-rw-r--r--	rewrite.v	3931	log plain
-rw-r--r--	rewrite_dep.v	929	log plain
-rw-r--r--	rewrite_in.v	148	log plain
-rw-r--r--	rewrite_iterated.v	545	log plain
-rw-r--r--	rewrite_strat.v	1274	log plain
-rw-r--r--	searchabout.v	1690	log plain
-rw-r--r--	set.v	408	log plain
-rw-r--r--	setoid_ring_module.v	922	log plain
-rw-r--r--	setoid_test.v	4346	log plain
-rw-r--r--	setoid_test2.v	8251	log plain
-rw-r--r--	setoid_test_function_space.v	1117	log plain
-rw-r--r--	setoid_unif.v	911	log plain
-rw-r--r--	shrink_abstract.v	220	log plain
-rw-r--r--	shrink_obligations.v	605	log plain
-rw-r--r--	sideff.v	277	log plain
-rw-r--r--	simpl.v	2695	log plain
-rw-r--r--	simpl_tuning.v	3895	log plain
-rw-r--r--	somatching.v	1534	log plain
-rw-r--r--	specialize.v	1960	log plain
-rw-r--r--	subst.v	591	log plain
-rw-r--r--	telescope_canonical.v	2393	log plain
-rw-r--r--	tryif.v	1331	log plain
-rw-r--r--	unfold.v	812	log plain
-rw-r--r--	unicode_utf8.v	2216	log plain
-rw-r--r--	unification.v	5958	log plain
-rw-r--r--	univers.v	1964	log plain
-rw-r--r--	universes-coercion.v	917	log plain
-rw-r--r--	univnames.v	733	log plain
-rw-r--r--	univscompute.v	721	log plain
-rw-r--r--	unshelve.v	216	log plain
-rw-r--r--	vm_univ_poly.v	4212	log plain
-rw-r--r--	vm_univ_poly_match.v	606	log plain