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--	CanonicalStructure.v	332	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	38268	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	206	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--	Generalize.v	176	log plain
-rw-r--r--	Hints.v	1261	log plain
-rw-r--r--	ImplicitArguments.v	514	log plain
-rw-r--r--	ImplicitTactic.v	549	log plain
-rw-r--r--	Inductive.v	1427	log plain
-rw-r--r--	Injection.v	1390	log plain
-rw-r--r--	Inversion.v	2676	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	755	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--	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	106	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--	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	4406	log plain
-rw-r--r--	Try.v	182	log plain
-rw-r--r--	apply.v	5439	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	1564	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	2280	log plain
-rw-r--r--	destruct.v	1089	log plain
-rw-r--r--	eauto.v	1868	log plain
-rw-r--r--	eqdecide.v	912	log plain
-rw-r--r--	evars.v	6522	log plain
-rw-r--r--	extraction.v	14264	log plain
-rw-r--r--	fix.v	2212	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	4393	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	379	log plain
-rw-r--r--	polymorphism.v	220	log plain
-rw-r--r--	refine.v	2551	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--	set.v	90	log plain
-rw-r--r--	setoid_ring_module.v	925	log plain
-rw-r--r--	setoid_test.v	2293	log plain
-rw-r--r--	setoid_test2.v	8269	log plain
-rw-r--r--	setoid_test_function_space.v	1434	log plain
-rw-r--r--	simpl.v	655	log plain
-rw-r--r--	specialize.v	1459	log plain
-rw-r--r--	unfold.v	644	log plain
-rw-r--r--	unicode_utf8.v	372	log plain
-rw-r--r--	unification.v	3912	log plain
-rw-r--r--	univers.v	1752	log plain