success « test-suite - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	Abstract.v	434	log plain
-rw-r--r--	AdvancedCanonicalStructure.v	3365	log plain
-rw-r--r--	AdvancedTypeClasses.v	2229	log plain
-rw-r--r--	BidirectionalityHints.v	3790	log plain
-rw-r--r--	BracketsWithGoalSelector.v	523	log plain
-rw-r--r--	CanonicalStructure.v	2507	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	3805	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	612	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	3235	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	991	log plain
-rw-r--r--	Cases.v	42411	log plain
-rw-r--r--	CasesDep.v	14537	log plain
-rw-r--r--	Cases_bug1834.v	382	log plain
-rw-r--r--	Cases_bug3758.v	386	log plain
-rw-r--r--	Check.v	964	log plain
-rw-r--r--	CombinedScheme.v	1318	log plain
-rw-r--r--	CompatCurrentFlag.v	163	log plain
-rw-r--r--	CompatOldFlag.v	225	log plain
-rw-r--r--	CompatOldOldFlag.v	253	log plain
-rw-r--r--	CompatPreviousFlag.v	199	log plain
-rw-r--r--	Conjecture.v	231	log plain
-rw-r--r--	ConversionOrder.v	513	log plain
-rw-r--r--	CumulInd.v	805	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--	Discriminate_HoTT.v	2488	log plain
-rw-r--r--	Field.v	2128	log plain
-rw-r--r--	Fixpoint.v	3258	log plain
-rw-r--r--	Funind.v	10178	log plain
-rw-r--r--	Generalization.v	489	log plain
-rw-r--r--	Generalize.v	176	log plain
-rw-r--r--	HintMode.v	674	log plain
-rw-r--r--	Hints.v	6002	log plain
-rw-r--r--	ImplicitArguments.v	1686	log plain
-rw-r--r--	Import.v	218	log plain
-rw-r--r--	Inductive.v	6421	log plain
-rw-r--r--	InductiveVsImplicitsVsTC.v	690	log plain
-rw-r--r--	Injection.v	4023	log plain
-rw-r--r--	Inversion.v	5365	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--	LocalDefinition.v	1244	log plain
-rw-r--r--	LraTest.v	285	log plain
-rw-r--r--	LtacDeprecation.v	473	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--	Nia.v	76592	log plain
-rw-r--r--	NotationDeprecation.v	508	log plain
-rw-r--r--	Notations.v	4808	log plain
-rw-r--r--	Notations2.v	7916	log plain
-rw-r--r--	NotationsAndLtac.v	1529	log plain
-rw-r--r--	Nsatz.v	14224	log plain
-rw-r--r--	NumberNotationsNoLocal.v	418	log plain
-rw-r--r--	NumberScopes.v	921	log plain
-rw-r--r--	Omega.v	2164	log plain
-rw-r--r--	Omega0.v	2395	log plain
-rw-r--r--	Omega2.v	761	log plain
-rw-r--r--	OmegaPre.v	1963	log plain
-rw-r--r--	PCase.v	1515	log plain
-rw-r--r--	PPFix.v	207	log plain
-rw-r--r--	PartialImport.v	965	log plain
-rw-r--r--	PatternsInBinders.v	1426	log plain
-rw-r--r--	Print.v	289	log plain
-rw-r--r--	PrintSortedUniverses.v	39	log plain
-rw-r--r--	ProgramWf.v	2267	log plain
-rw-r--r--	Projection.v	1278	log plain
-rw-r--r--	ROmega.v	2276	log plain
-rw-r--r--	ROmega0.v	2784	log plain
-rw-r--r--	ROmega2.v	1113	log plain
-rw-r--r--	ROmega4.v	479	log plain
-rw-r--r--	ROmegaPre.v	1828	log plain
-rw-r--r--	RecTutorial.v	25134	log plain
-rw-r--r--	Record.v	2939	log plain
-rw-r--r--	RefineInstance.v	435	log plain
-rw-r--r--	Reg.v	3062	log plain
-rw-r--r--	Remark.v	172	log plain
-rw-r--r--	RemoteUnivs.v	368	log plain
-rw-r--r--	Rename.v	222	log plain
-rw-r--r--	Reordering.v	379	log plain
-rw-r--r--	Require.v	210	log plain
-rw-r--r--	RewriteRegisteredElim.v	949	log plain
-rw-r--r--	Scheme.v	785	log plain
-rw-r--r--	SchemeEquality.v	734	log plain
-rw-r--r--	Scopes.v	833	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--	Template.v	4475	log plain
-rw-r--r--	TestRefine.v	4465	log plain
-rw-r--r--	Try.v	172	log plain
-rw-r--r--	Typeclasses.v	8224	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	15550	log plain
-rw-r--r--	applyTC.v	289	log plain
-rw-r--r--	attribute_syntax.v	1101	log plain
-rw-r--r--	auto.v	3359	log plain
-rw-r--r--	autointros.v	433	log plain
-rw-r--r--	autorewrite.v	949	log plain
-rw-r--r--	boundvars.v	621	log plain
-rw-r--r--	btauto.v	219	log plain
-rw-r--r--	bteauto.v	4131	log plain
-rw-r--r--	bug_10890.v	206	log plain
-rw-r--r--	bullet.v	53	log plain
-rw-r--r--	case_let_conversion.v	813	log plain
-rw-r--r--	case_let_param.v	281	log plain
-rw-r--r--	cbn.v	317	log plain
-rw-r--r--	cbv_let.v	665	log plain
-rw-r--r--	cc.v	3472	log plain
-rw-r--r--	change.v	2094	log plain
-rw-r--r--	change_case.v	417	log plain
-rw-r--r--	change_pattern.v	1251	log plain
-rw-r--r--	clear.v	568	log plain
-rw-r--r--	coercions.v	5022	log plain
-rw-r--r--	cofixtac.v	209	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	4387	log plain
-rw-r--r--	custom_entry.v	236	log plain
-rw-r--r--	definition_using.v	1211	log plain
-rw-r--r--	dependentind.v	3924	log plain
-rw-r--r--	destruct.v	9894	log plain
-rw-r--r--	dtauto_let_deps.v	792	log plain
-rw-r--r--	eauto.v	5826	log plain
-rw-r--r--	eqdecide.v	1188	log plain
-rw-r--r--	eqtacticsnois.v	355	log plain
-rw-r--r--	eta.v	595	log plain
-rw-r--r--	evars.v	13740	log plain
-rw-r--r--	export_hint.v	203	log plain
-rw-r--r--	extraction.v	15165	log plain
-rw-r--r--	extraction_dep.v	990	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	2174	log plain
-rw-r--r--	forward.v	718	log plain
-rw-r--r--	goal_selector.v	1422	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	366	log plain
-rw-r--r--	implicit.v	4404	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	4298	log plain
-rw-r--r--	intros.v	3508	log plain
-rw-r--r--	keyedrewrite.v	1378	log plain
-rw-r--r--	let_pattern_mismatch.v	592	log plain
-rw-r--r--	let_universes.v	88	log plain
-rw-r--r--	letproj.v	307	log plain
-rw-r--r--	ltac.v	8494	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	764	log plain
-rw-r--r--	match_case_pattern_variables.v	789	log plain
-rw-r--r--	module_with_def_univ_poly.v	669	log plain
-rw-r--r--	mutual_ind.v	1751	log plain
-rw-r--r--	mutual_record.v	753	log plain
-rw-r--r--	name_mangling.v	3171	log plain
-rw-r--r--	namedunivs.v	2825	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	11029	log plain
-rw-r--r--	pose.v	141	log plain
-rw-r--r--	primitive.v	2192	log plain
-rw-r--r--	primitiveproj.v	5528	log plain
-rw-r--r--	private_univs.v	1230	log plain
-rw-r--r--	programequality.v	267	log plain
-rw-r--r--	proof_using.v	2575	log plain
-rw-r--r--	proof_using_noinit.v	136	log plain
-rw-r--r--	rapply.v	892	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	4315	log plain
-rw-r--r--	rewrite_dep.v	930	log plain
-rw-r--r--	rewrite_evar.v	383	log plain
-rw-r--r--	rewrite_in.v	284	log plain
-rw-r--r--	rewrite_iterated.v	541	log plain
-rw-r--r--	rewrite_strat.v	1520	log plain
-rw-r--r--	search.v	797	log plain
-rw-r--r--	section_poly.v	1402	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	8547	log plain
-rw-r--r--	setoid_test_function_space.v	1117	log plain
-rw-r--r--	setoid_unif.v	918	log plain
-rw-r--r--	shrink_abstract.v	198	log plain
-rw-r--r--	shrink_obligations.v	580	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	4300	log plain
-rw-r--r--	sprop.v	5688	log plain
-rw-r--r--	sprop_hcons.v	1378	log plain
-rw-r--r--	sprop_uip.v	4180	log plain
-rw-r--r--	ssrpattern.v	514	log plain
-rw-r--r--	strategy.v	1997	log plain
-rw-r--r--	subst.v	984	log plain
-rw-r--r--	tac_wit_ref.v	116	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--	typing_flags.v	2551	log plain
-rw-r--r--	unfold.v	2093	log plain
-rw-r--r--	unicode_utf8.v	2216	log plain
-rw-r--r--	unidecls.v	2262	log plain
-rw-r--r--	unification.v	6301	log plain
-rw-r--r--	uniform_inductive_parameters.v	661	log plain
-rw-r--r--	univers.v	1942	log plain
-rw-r--r--	universes_coercion.v	914	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_records.v	635	log plain
-rw-r--r--	vm_univ_poly.v	4178	log plain
-rw-r--r--	vm_univ_poly_match.v	606	log plain
-rw-r--r--	with_strategy.v	22907	log plain