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

Mode	Name	Size
-rw-r--r--	Abstract.v	445	log plain
-rw-r--r--	AdvancedCanonicalStructure.v	2844	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	341	log plain
-rw-r--r--	Case12.v	2072	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	405	log plain
-rw-r--r--	Case17.v	1844	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--	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	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	38254	log plain
-rw-r--r--	CasesDep.v	12959	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	644	log plain
-rw-r--r--	Field.v	1978	log plain
-rw-r--r--	Fixpoint.v	2343	log plain
-rw-r--r--	Fourier.v	281	log plain
-rw-r--r--	Funind.v	10127	log plain
-rw-r--r--	Generalization.v	282	log plain
-rw-r--r--	Generalize.v	176	log plain
-rw-r--r--	Hints.v	1866	log plain
-rw-r--r--	ImplicitArguments.v	545	log plain
-rw-r--r--	ImplicitTactic.v	549	log plain
-rw-r--r--	Import.v	218	log plain
-rw-r--r--	Inductive.v	2966	log plain
-rw-r--r--	Injection.v	1768	log plain
-rw-r--r--	Inversion.v	3709	log plain
-rw-r--r--	LegacyField.v	1706	log plain
-rw-r--r--	LetIn.v	356	log plain
-rw-r--r--	LetPat.v	1750	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	2041	log plain
-rw-r--r--	Nsatz.v	14259	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	2182	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	2053	log plain
-rw-r--r--	Projection.v	1151	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	2203	log plain
-rw-r--r--	RecTutorial.v	25343	log plain
-rw-r--r--	Record.v	2399	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--	Scheme.v	82	log plain
-rw-r--r--	Scopes.v	157	log plain
-rw-r--r--	Section.v	136	log plain
-rw-r--r--	Simplify_eq.v	252	log plain
-rw-r--r--	Tauto.v	5145	log plain
-rw-r--r--	TestRefine.v	4315	log plain
-rw-r--r--	Try.v	182	log plain
-rw-r--r--	Typeclasses.v	1458	log plain
-rw-r--r--	apply.v	10147	log plain
-rw-r--r--	auto.v	548	log plain
-rw-r--r--	autointros.v	462	log plain
-rw-r--r--	autorewrite.v	763	log plain
-rw-r--r--	bullet.v	53	log plain
-rw-r--r--	cc.v	2331	log plain
-rw-r--r--	change.v	1105	log plain
-rw-r--r--	clear.v	290	log plain
-rw-r--r--	coercions.v	2120	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	5527	log plain
-rw-r--r--	dependentind.v	3341	log plain
-rw-r--r--	destruct.v	1780	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	7942	log plain
-rw-r--r--	extraction.v	14182	log plain
-rw-r--r--	fix.v	2168	log plain
-rw-r--r--	guard.v	322	log plain
-rw-r--r--	hyps_inclusion.v	1150	log plain
-rw-r--r--	if.v	366	log plain
-rw-r--r--	implicit.v	2648	log plain
-rw-r--r--	import_lib.v	3415	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	1783	log plain
-rw-r--r--	instantiate.v	292	log plain
-rw-r--r--	intros.v	168	log plain
-rw-r--r--	ltac.v	6259	log plain
-rw-r--r--	mutual_ind.v	1601	log plain
-rw-r--r--	options.v	690	log plain
-rw-r--r--	params_ind.v	93	log plain
-rw-r--r--	parsing.v	218	log plain
-rw-r--r--	pattern.v	1400	log plain
-rw-r--r--	polymorphism.v	219	log plain
-rw-r--r--	refine.v	2661	log plain
-rw-r--r--	replace.v	635	log plain
-rw-r--r--	rewrite.v	3009	log plain
-rw-r--r--	rewrite_in.v	148	log plain
-rw-r--r--	rewrite_iterated.v	545	log plain
-rw-r--r--	searchabout.v	1690	log plain
-rw-r--r--	set.v	90	log plain
-rw-r--r--	setoid_ring_module.v	922	log plain
-rw-r--r--	setoid_test.v	3974	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--	simpl.v	1232	log plain
-rw-r--r--	specialize.v	1458	log plain
-rw-r--r--	unfold.v	812	log plain
-rw-r--r--	unicode_utf8.v	2172	log plain
-rw-r--r--	unification.v	5809	log plain
-rw-r--r--	univers.v	1591	log plain
-rw-r--r--	universes-coercion.v	917	log plain