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

Mode	Name	Size
-rw-r--r--	Abstract.v	438	log plain
-rw-r--r--	AdvancedCanonicalStructure.v	3365	log plain
-rw-r--r--	AdvancedTypeClasses.v	2235	log plain
-rw-r--r--	BracketsWithGoalSelector.v	371	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	2476	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	970	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	2646	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	984	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	39497	log plain
-rw-r--r--	CasesDep.v	14537	log plain
-rw-r--r--	Check.v	964	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	822	log plain
-rw-r--r--	Field.v	2128	log plain
-rw-r--r--	Fixpoint.v	2347	log plain
-rw-r--r--	Fourier.v	281	log plain
-rw-r--r--	Funind.v	10180	log plain
-rw-r--r--	FunindExtraction_compat86.v	10204	log plain
-rw-r--r--	Generalization.v	282	log plain
-rw-r--r--	Generalize.v	176	log plain
-rw-r--r--	Hints.v	5443	log plain
-rw-r--r--	ImplicitArguments.v	1053	log plain
-rw-r--r--	Import.v	218	log plain
-rw-r--r--	Inductive.v	6083	log plain
-rw-r--r--	Injection.v	4023	log plain
-rw-r--r--	Inversion.v	5366	log plain
-rw-r--r--	InversionSigma.v	1574	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	515	log plain
-rw-r--r--	NatRing.v	125	log plain
-rw-r--r--	Notations.v	4808	log plain
-rw-r--r--	Notations2.v	6138	log plain
-rw-r--r--	Nsatz.v	14291	log plain
-rw-r--r--	NumberScopes.v	921	log plain
-rw-r--r--	Omega.v	2193	log plain
-rw-r--r--	Omega0.v	2429	log plain
-rw-r--r--	Omega2.v	765	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--	PatternsInBinders.v	1426	log plain
-rw-r--r--	Print.v	282	log plain
-rw-r--r--	PrintSortedUniverses.v	39	log plain
-rw-r--r--	ProgramWf.v	2279	log plain
-rw-r--r--	Projection.v	1278	log plain
-rw-r--r--	ROmega.v	2238	log plain
-rw-r--r--	ROmega0.v	2757	log plain
-rw-r--r--	ROmega2.v	984	log plain
-rw-r--r--	ROmega3.v	872	log plain
-rw-r--r--	ROmega4.v	488	log plain
-rw-r--r--	ROmegaPre.v	2216	log plain
-rw-r--r--	RecTutorial.v	25138	log plain
-rw-r--r--	Record.v	2598	log plain
-rw-r--r--	Reg.v	3062	log plain
-rw-r--r--	Remark.v	172	log plain
-rw-r--r--	Rename.v	222	log plain
-rw-r--r--	Reordering.v	378	log plain
-rw-r--r--	Require.v	88	log plain
-rw-r--r--	Scheme.v	593	log plain
-rw-r--r--	Scopes.v	561	log plain
-rw-r--r--	Section.v	136	log plain
-rw-r--r--	ShowExtraction.v	592	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	5295	log plain
-rw-r--r--	TestRefine.v	4465	log plain
-rw-r--r--	Try.v	172	log plain
-rw-r--r--	Typeclasses.v	6713	log plain
-rw-r--r--	abstract_chain.v	885	log plain
-rw-r--r--	abstract_poly.v	513	log plain
-rw-r--r--	all-check.v	36	log plain
-rw-r--r--	apply.v	14140	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--	boundvars.v	621	log plain
-rw-r--r--	bteauto.v	4062	log plain
-rw-r--r--	bullet.v	53	log plain
-rw-r--r--	cbn.v	317	log plain
-rw-r--r--	cc.v	3472	log plain
-rw-r--r--	change.v	1853	log plain
-rw-r--r--	change_pattern.v	1244	log plain
-rw-r--r--	clear.v	568	log plain
-rw-r--r--	coercions.v	5022	log plain
-rw-r--r--	coindprim.v	2826	log plain
-rw-r--r--	contradiction.v	563	log plain
-rw-r--r--	conv_pbs.v	7579	log plain
-rw-r--r--	coqbugs0181.v	211	log plain
-rw-r--r--	cumulativity.v	4162	log plain
-rw-r--r--	dependentind.v	3924	log plain
-rw-r--r--	destruct.v	9888	log plain
-rw-r--r--	dtauto-let-deps.v	792	log plain
-rw-r--r--	eauto.v	5790	log plain
-rw-r--r--	eqdecide.v	1188	log plain
-rw-r--r--	eta.v	595	log plain
-rw-r--r--	evars.v	13575	log plain
-rw-r--r--	extraction.v	15165	log plain
-rw-r--r--	extraction_dep.v	991	log plain
-rw-r--r--	extraction_impl.v	1922	log plain
-rw-r--r--	extraction_polyprop.v	398	log plain
-rw-r--r--	fix.v	2182	log plain
-rw-r--r--	forward.v	664	log plain
-rw-r--r--	goal_selector.v	1416	log plain
-rw-r--r--	guard.v	828	log plain
-rw-r--r--	hintdb_in_ltac.v	275	log plain
-rw-r--r--	hintdb_in_ltac_bis.v	237	log plain
-rw-r--r--	hyps_inclusion.v	1160	log plain
-rw-r--r--	if.v	365	log plain
-rw-r--r--	implicit.v	2768	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	1360	log plain
-rw-r--r--	inds_type_sec.v	744	log plain
-rw-r--r--	induct.v	5043	log plain
-rw-r--r--	intros.v	3285	log plain
-rw-r--r--	keyedrewrite.v	1384	log plain
-rw-r--r--	letproj.v	230	log plain
-rw-r--r--	ltac.v	7320	log plain
-rw-r--r--	ltac_match_pattern_names.v	604	log plain
-rw-r--r--	ltac_plus.v	357	log plain
-rw-r--r--	ltacprof.v	223	log plain
-rw-r--r--	mutual_ind.v	1751	log plain
-rw-r--r--	name_mangling.v	3289	log plain
-rw-r--r--	namedunivs.v	2799	log plain
-rw-r--r--	onlyprinting.v	150	log plain
-rw-r--r--	options.v	690	log plain
-rw-r--r--	par_abstract.v	469	log plain
-rw-r--r--	paralleltac.v	1193	log plain
-rw-r--r--	parsing.v	218	log plain
-rw-r--r--	pattern.v	1400	log plain
-rw-r--r--	polymorphism.v	11008	log plain
-rw-r--r--	primitiveproj.v	4666	log plain
-rw-r--r--	programequality.v	267	log plain
-rw-r--r--	proof_using.v	2575	log plain
-rw-r--r--	record_syntax.v	920	log plain
-rw-r--r--	refine.v	2992	log plain
-rw-r--r--	remember.v	626	log plain
-rw-r--r--	replace.v	635	log plain
-rw-r--r--	rewrite.v	4318	log plain
-rw-r--r--	rewrite_dep.v	930	log plain
-rw-r--r--	rewrite_evar.v	376	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	1275	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	4488	log plain
-rw-r--r--	setoid_test2.v	8535	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	198	log plain
-rw-r--r--	shrink_obligations.v	605	log plain
-rw-r--r--	sideff.v	305	log plain
-rw-r--r--	simpl.v	2693	log plain
-rw-r--r--	simpl_tuning.v	3897	log plain
-rw-r--r--	somatching.v	1534	log plain
-rw-r--r--	specialize.v	3465	log plain
-rw-r--r--	ssr_delayed_clear_rename.v	128	log plain
-rw-r--r--	ssrpattern.v	514	log plain
-rw-r--r--	subst.v	984	log plain
-rw-r--r--	telescope_canonical.v	2393	log plain
-rw-r--r--	transparent_abstract.v	800	log plain
-rw-r--r--	tryif.v	1331	log plain
-rw-r--r--	unfold.v	962	log plain
-rw-r--r--	unicode_utf8.v	2216	log plain
-rw-r--r--	unidecls.v	2228	log plain
-rw-r--r--	unification.v	6301	log plain
-rw-r--r--	univers.v	1943	log plain
-rw-r--r--	universes-coercion.v	917	log plain
-rw-r--r--	univnames.v	904	log plain
-rw-r--r--	univscompute.v	721	log plain
-rw-r--r--	unshelve.v	401	log plain
-rw-r--r--	vm_evars.v	348	log plain
-rw-r--r--	vm_univ_poly.v	4178	log plain
-rw-r--r--	vm_univ_poly_match.v	606	log plain