Folder: success

package info (click to toggle)

coq 8.20.1%2Bdfsg-1

links: PTS, VCS
area: main
in suites: sid, trixie
size: 44,116 kB
sloc: ml: 234,160; sh: 4,301; python: 3,270; ansic: 2,644; makefile: 882; lisp: 172; javascript: 63; xml: 24; sed: 2

			.. (parent)
-	rw-r--r--	434	Abstract.v
-	rw-r--r--	3,365	AdvancedCanonicalStructure.v
-	rw-r--r--	2,229	AdvancedTypeClasses.v
-	rw-r--r--	1,788	Assumptions.v
-	rw-r--r--	263	AutoPropLowering.v
-	rw-r--r--	3,790	BidirectionalityHints.v
-	rw-r--r--	523	BracketsWithGoalSelector.v
-	rw-r--r--	6,966	CanonicalStructure.v
-	rw-r--r--	335	Case1.v
-	rw-r--r--	738	Case10.v
-	rw-r--r--	349	Case11.v
-	rw-r--r--	2,083	Case12.v
-	rw-r--r--	3,805	Case13.v
-	rw-r--r--	510	Case14.v
-	rw-r--r--	1,315	Case15.v
-	rw-r--r--	409	Case16.v
-	rw-r--r--	1,861	Case17.v
-	rw-r--r--	612	Case18.v
-	rw-r--r--	972	Case19.v
-	rw-r--r--	306	Case2.v
-	rw-r--r--	1,106	Case20.v
-	rw-r--r--	476	Case21.v
-	rw-r--r--	3,235	Case22.v
-	rw-r--r--	720	Case3.v
-	rw-r--r--	1,201	Case4.v
-	rw-r--r--	365	Case5.v
-	rw-r--r--	583	Case6.v
-	rw-r--r--	478	Case7.v
-	rw-r--r--	338	Case8.v
-	rw-r--r--	2,269	Case9.v
-	rw-r--r--	2,598	CaseAlias.v
-	rw-r--r--	245	CaseCumul.v
-	rw-r--r--	991	CaseInClause.v
-	rw-r--r--	42,411	Cases.v
-	rw-r--r--	14,512	CasesDep.v
-	rw-r--r--	382	Cases_bug1834.v
-	rw-r--r--	386	Cases_bug3758.v
-	rw-r--r--	964	Check.v
-	rw-r--r--	1,318	CombinedScheme.v
-	rw-r--r--	163	CompatCurrentFlag.v
-	rw-r--r--	225	CompatOldFlag.v
-	rw-r--r--	199	CompatPreviousFlag.v
-	rw-r--r--	231	Conjecture.v
-	rw-r--r--	513	ConversionOrder.v
-	rw-r--r--	1,493	CumulInd.v
-	rw-r--r--	1	DHyp.v
-	rw-r--r--	218	Decompose.v
-	rw-r--r--	160	DependentPropositionEliminators.v
-	rw-r--r--	162	DisableVM.v
-	rw-r--r--	435	DiscrR.v
-	rw-r--r--	822	Discriminate.v
-	rw-r--r--	2,507	Discriminate_HoTT.v
-	rw-r--r--	2,128	Field.v
-	rw-r--r--	655	FinalObligation.v
-	rw-r--r--	2,051	FixStronglyWf.v
-	rw-r--r--	14,684	Fixpoint.v
-	rw-r--r--	10,543	Funind.v
-	rw-r--r--	490	Generalization.v
-	rw-r--r--	176	Generalize.v
-	rw-r--r--	1,863	HintMode.v
-	rw-r--r--	5,946	Hints.v
-	rw-r--r--	1,686	ImplicitArguments.v
-	rw-r--r--	218	Import.v
-	rw-r--r--	1,602	ImportCat.v
-	rw-r--r--	6,421	Inductive.v
-	rw-r--r--	700	InductiveVsImplicitsVsTC.v
-	rw-r--r--	4,023	Injection.v
-	rw-r--r--	5,365	Inversion.v
-	rw-r--r--	9,919	InversionSigma.v
-	rw-r--r--	356	LetIn.v
-	rw-r--r--	1,761	LetPat.v
-	rw-r--r--	1,326	LocalDefinition.v
-	rw-r--r--	285	LraTest.v
-	rw-r--r--	473	LtacDeprecation.v
-	rw-r--r--	570	MangleNamesLight.v
-	rw-r--r--	844	MatchFail.v
-	rw-r--r--	302	Mod_ltac.v
-	rw-r--r--	1,375	Mod_params.v
-	rw-r--r--	963	Mod_strengthen.v
-	rw-r--r--	515	Mod_type.v
-	rw-r--r--	125	NatRing.v
-	rw-r--r--	5,933	NestedInd.v
-	rw-r--r--	651	NotationDeprecation.v
-	rw-r--r--	5,281	Notations.v
-	rw-r--r--	8,826	Notations2.v
-	rw-r--r--	1,529	NotationsAndLtac.v
-	rw-r--r--	14,231	Nsatz.v
-	rw-r--r--	418	NumberNotationsNoLocal.v
-	rw-r--r--	921	NumberScopes.v
-	rw-r--r--	2,164	Omega.v
-	rw-r--r--	2,395	Omega0.v
-	rw-r--r--	761	Omega2.v
-	rw-r--r--	1,963	OmegaPre.v
-	rw-r--r--	1,515	PCase.v
-	rw-r--r--	239	PPFix.v
-	rw-r--r--	2,074	PartialImport.v
-	rw-r--r--	1,426	PatternsInBinders.v
-	rw-r--r--	289	Print.v
-	rw-r--r--	39	PrintSortedUniverses.v
-	rw-r--r--	779	PrivateInd.v
-	rw-r--r--	1,111	ProgramCases.v
-	rw-r--r--	3,083	ProgramWf.v
-	rw-r--r--	1,278	Projection.v
-	rw-r--r--	2,276	ROmega.v
-	rw-r--r--	2,784	ROmega0.v
-	rw-r--r--	1,113	ROmega2.v
-	rw-r--r--	479	ROmega4.v
-	rw-r--r--	1,828	ROmegaPre.v
-	rw-r--r--	25,164	RecTutorial.v
-	rw-r--r--	3,213	Record.v
-	rw-r--r--	479	RefineInstance.v
-	rw-r--r--	3,062	Reg.v
-	rw-r--r--	172	Remark.v
-	rw-r--r--	368	RemoteUnivs.v
-	rw-r--r--	222	Rename.v
-	rw-r--r--	379	Reordering.v
-	rw-r--r--	192	Require.v
-	rw-r--r--	949	RewriteRegisteredElim.v
-	rw-r--r--	785	Scheme.v
-	rw-r--r--	11,879	SchemeEquality.v
-	rw-r--r--	1,096	Scopes.v
-	rw-r--r--	136	Section.v
-	rw-r--r--	592	ShowExtraction.v
-	rw-r--r--	252	Simplify_eq.v
-	rw-r--r--	749	StuckHintMode.v
-	rw-r--r--	2,651	TCbacktrack.v
-	rw-r--r--	198	TacticNotation1.v
-	rw-r--r--	310	TacticNotation2.v
-	rw-r--r--	5,295	Tauto.v
-	rw-r--r--	5,559	Template.v
-	rw-r--r--	4,453	TestRefine.v
-	rw-r--r--	172	Try.v
-	rw-r--r--	9,239	Typeclasses.v
-	rw-r--r--	2,180	TypeclassesOpaque.v
-	rw-r--r--	1,155	Typeclasses_eauto_dfs_bfs.v
-	rw-r--r--	276	ValidateProof.v
-	rw-r--r--	35,910	ZModulo.v
-	rw-r--r--	885	abstract_chain.v
-	rw-r--r--	513	abstract_poly.v
-	rw-r--r--	591	abstract_with_evars.v
-	rw-r--r--	36	all_check.v
-	rw-r--r--	15,355	apply.v
-	rw-r--r--	299	applyTC.v
-	rw-r--r--	1,102	attribute_syntax.v
-	rw-r--r--	3,468	auto.v
-	rw-r--r--	433	autointros.v
-	rw-r--r--	950	autorewrite.v
-	rw-r--r--	621	boundvars.v
-	rw-r--r--	219	btauto.v
-	rw-r--r--	4,323	bteauto.v
-	rw-r--r--	206	bug_10890.v
-	rw-r--r--	590	bug_14174.v
-	rw-r--r--	53	bullet.v
-	rw-r--r--	813	case_let_conversion.v
-	rw-r--r--	281	case_let_param.v
-	rw-r--r--	1,677	cbn.v
-	rw-r--r--	665	cbv_let.v
-	rw-r--r--	3,472	cc.v
-	rw-r--r--	2,094	change.v
-	rw-r--r--	417	change_case.v
-	rw-r--r--	1,251	change_pattern.v
-	rw-r--r--	568	clear.v
-	rw-r--r--	6,364	coercions.v
-	rw-r--r--	209	cofixtac.v
-	rw-r--r--	2,826	coindprim.v
-	rw-r--r--	563	contradiction.v
-	rw-r--r--	7,581	conv_pbs.v
-	rw-r--r--	4,802	cumulativity.v
-	rw-r--r--	236	custom_entry.v
-	rw-r--r--	2,846	definition_using.v
-	rw-r--r--	3,936	dependentind.v
-	rw-r--r--	9,906	destruct.v
-	rw-r--r--	794	dtauto_let_deps.v
-	rw-r--r--	284	eapply_evar.v
-	rw-r--r--	5,960	eauto.v
-	rw-r--r--	1,188	eqdecide.v
-	rw-r--r--	355	eqtacticsnois.v
-	rw-r--r--	595	eta.v
-	rw-r--r--	13,752	evars.v
-	rw-r--r--	203	export_hint.v
-	rw-r--r--	546	export_inst.v
-	rw-r--r--	222	extra_dep.v
-	rw-r--r--	154	extra_dep2.v
-	rw-r--r--	16,590	extraction.v
-	rw-r--r--	2,541	extraction_bigint.v
-	rw-r--r--	990	extraction_dep.v
-	rw-r--r--	1,922	extraction_impl.v
-	rw-r--r--	398	extraction_polyprop.v
-	rw-r--r--	2,756	fix.v
-	rw-r--r--	718	forward.v
-	rw-r--r--	203	freshness.v
-	rw-r--r--	1,485	goal_selector.v
-	rw-r--r--	828	guard.v
-	rw-r--r--	636	hint_discr_unfold.v
-	rw-r--r--	285	hintdb_in_ltac.v
-	rw-r--r--	247	hintdb_in_ltac_bis.v
-	rw-r--r--	1,160	hyps_inclusion.v
-	rw-r--r--	366	if.v
-	rw-r--r--	4,760	implicit.v
-	rw-r--r--	3,618	import_lib.v
-	rw-r--r--	993	import_mod.v
-	rw-r--r--	1,360	indelim.v
-	rw-r--r--	744	inds_type_sec.v
-	rw-r--r--	4,298	induct.v
-	rw-r--r--	139	instantiate.v
-	rw-r--r--	3,526	intros.v
-	rw-r--r--	1,378	keyedrewrite.v
-	rw-r--r--	592	let_pattern_mismatch.v
-	rw-r--r--	88	let_universes.v
-	rw-r--r--	307	letproj.v
-	rw-r--r--	10,802	locality_attributes_modules.v
-	rw-r--r--	3,483	locality_attributes_modules_ltac2.v
-	rw-r--r--	7,068	locality_attributes_sections.v
-	rw-r--r--	5,245	locality_attributes_sections_in_modules.v
-	rw-r--r--	2,784	locality_attributes_sections_ltac2.v
-	rw-r--r--	9,815	ltac.v
-	rw-r--r--	604	ltac_match_pattern_names.v
-	rw-r--r--	357	ltac_plus.v
-	rw-r--r--	764	ltacprof.v
-	rw-r--r--	789	match_case_pattern_variables.v
-	rw-r--r--	669	module_with_def_univ_poly.v
-	rw-r--r--	1,752	mutual_ind.v
-	rw-r--r--	753	mutual_record.v
-	rw-r--r--	3,171	name_mangling.v
-	rw-r--r--	2,825	namedunivs.v
-	rw-r--r--	127	nativecompute.v
-	rw-r--r--	150	onlyprinting.v
-	rw-r--r--	690	options.v
-	rw-r--r--	469	par_abstract.v
-	rw-r--r--	1,209	paralleltac.v
-	rw-r--r--	218	parsing.v
-	rw-r--r--	1,400	pattern.v
-	rw-r--r--	130	pattern_genarg.v
-	rw-r--r--	11,323	polymorphism.v
-	rw-r--r--	141	pose.v
-	rw-r--r--	2,192	primitive.v
-	rw-r--r--	525	primitive_strategy.v
-	rw-r--r--	3,213	primitive_tc.v
-	rw-r--r--	6,575	primitiveproj.v
-	rw-r--r--	742	primproj_evarconv.v
-	rw-r--r--	1,380	primproj_ssreflect.v
-	rw-r--r--	3,047	primproj_tactic_unif.v
-	rw-r--r--	1,230	private_univs.v
-	rw-r--r--	267	programequality.v
-	rw-r--r--	3,870	proof_using.v
-	rw-r--r--	136	proof_using_noinit.v
-	rw-r--r--	892	rapply.v
-	rw-r--r--	920	record_syntax.v
-	rw-r--r--	2,992	refine.v
-	rw-r--r--	626	remember.v
-	rw-r--r--	635	replace.v
-	rw-r--r--	494	resolve_tc.v
-	rw-r--r--	3,552	reverse_coercions.v
-	rw-r--r--	1,411	reverse_coercions_ac.v
-	rw-r--r--	938	reverse_coercions_typeclasses_and_canonical.v
-	rw-r--r--	4,318	rewrite.v
-	rw-r--r--	1,240	rewrite_closed.v
-	rw-r--r--	951	rewrite_dep.v
-	rw-r--r--	383	rewrite_evar.v
-	rw-r--r--	284	rewrite_in.v
-	rw-r--r--	541	rewrite_iterated.v
-	rw-r--r--	1,728	rewrite_strat.v
-	rw-r--r--	9,340	rewrule.v
-	rw-r--r--	710	rewrule_quality_match.v
-	rw-r--r--	793	search.v
-	rw-r--r--	1,402	section_poly.v
-	rw-r--r--	741	set.v
-	rw-r--r--	922	setoid_ring_module.v
-	rw-r--r--	8,536	setoid_test.v
-	rw-r--r--	8,567	setoid_test2.v
-	rw-r--r--	1,139	setoid_test_function_space.v
-	rw-r--r--	918	setoid_unif.v
-	rw-r--r--	198	shrink_abstract.v
-	rw-r--r--	580	shrink_obligations.v
-	rw-r--r--	305	sideff.v
-	rw-r--r--	10,802	simpl.v
-	rw-r--r--	3,900	simpl_tuning.v
-	rw-r--r--	2,190	simple_congruence.v
-	rw-r--r--	1,534	somatching.v
-	rw-r--r--	8,767	sort_poly.v
-	rw-r--r--	534	sort_poly_extraction.v
-	rw-r--r--	5,674	specialize.v
-	rw-r--r--	5,556	sprop.v
-	rw-r--r--	504	sprop_fast.v
-	rw-r--r--	1,378	sprop_hcons.v
-	rw-r--r--	4,180	sprop_uip.v
-	rw-r--r--	514	ssrpattern.v
-	rw-r--r--	1,997	strategy.v
-	rw-r--r--	2,481	strong_and_binary_induction.v
-	rw-r--r--	217	subprf_commands.v
-	rw-r--r--	984	subst.v
-	rw-r--r--	116	tac_wit_ref.v
-	rw-r--r--	2,393	telescope_canonical.v
-	rw-r--r--	810	transparent_abstract.v
-	rw-r--r--	1,331	tryif.v
-	rw-r--r--	2,686	typing_flags.v
-	rw-r--r--	2,093	unfold.v
-	rw-r--r--	2,216	unicode_utf8.v
-	rw-r--r--	2,262	unidecls.v
-	rw-r--r--	6,427	unification.v
-	rw-r--r--	1,130	unification_delta.v
-	rw-r--r--	661	uniform_inductive_parameters.v
-	rw-r--r--	1,943	univers.v
-	rw-r--r--	914	universes_coercion.v
-	rw-r--r--	934	univnames.v
-	rw-r--r--	721	univscompute.v
-	rw-r--r--	524	unknown_warning.v
-	rw-r--r--	796	unshelve.v
-	rw-r--r--	348	vm_evars.v
-	rw-r--r--	1,197	vm_norm_records.v
-	rw-r--r--	635	vm_records.v
-	rw-r--r--	4,194	vm_univ_poly.v
-	rw-r--r--	606	vm_univ_poly_match.v
-	rw-r--r--	177	warnings_attribute.v
-	rw-r--r--	22,907	with_strategy.v