Folder: output

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)
d	rwxr-xr-x	69	load
-	rw-r--r--	4,564	Arguments.out
-	rw-r--r--	2,005	Arguments.v
-	rw-r--r--	2,900	ArgumentsScope.out
-	rw-r--r--	2,380	ArgumentsScope.v
-	rw-r--r--	4,636	Arguments_renaming.out
-	rw-r--r--	1,196	Arguments_renaming.v
-	rw-r--r--	1,095	BadOptionValueType.out
-	rw-r--r--	183	BadOptionValueType.v
-	rw-r--r--	384	BinaryPrintingNotations.out
-	rw-r--r--	18,437	BinaryPrintingNotations.v
-	rw-r--r--	206	Binder.out
-	rw-r--r--	134	Binder.v
-	rw-r--r--	899	CantApplyBadType.out
-	rw-r--r--	843	CantApplyBadType.v
-	rw-r--r--	8,941	Cases.out
-	rw-r--r--	9,076	Cases.v
-	rw-r--r--	209	ClassMissingInstance.out
-	rw-r--r--	133	ClassMissingInstance.v
-	rw-r--r--	284	CoercionOnHole.out
-	rw-r--r--	482	CoercionOnHole.v
-	rw-r--r--	108	Coercions.out
-	rw-r--r--	651	Coercions.v
-	rw-r--r--	139	CompactContexts.out
-	rw-r--r--	141	CompactContexts.v
-	rw-r--r--	207	DebugFlags.out
-	rw-r--r--	72	DebugFlags.v
-	rw-r--r--	1,296	DebugRelevances.out
-	rw-r--r--	1,183	DebugRelevances.v
-	rw-r--r--	408	DependentInductionErrors.out
-	rw-r--r--	379	DependentInductionErrors.v
-	rw-r--r--	680	Deprecation.out
-	rw-r--r--	342	Deprecation.v
-	rw-r--r--	0	Emacs_and_diffs.out
-	rw-r--r--	100	Emacs_and_diffs.v
-	rw-r--r--	648	EmptyExtraction.out
-	rw-r--r--	1,016	EmptyExtraction.v
-	rw-r--r--	167	EqNotation.out
-	rw-r--r--	83	EqNotation.v
-	rw-r--r--	414	ErrorInCanonicalStructures.out
-	rw-r--r--	144	ErrorInCanonicalStructures.v
-	rw-r--r--	171	ErrorInModule.out
-	rw-r--r--	104	ErrorInModule.v
-	rw-r--r--	172	ErrorInSection.out
-	rw-r--r--	105	ErrorInSection.v
-	rw-r--r--	292	ErrorLocation_12152.out
-	rw-r--r--	84	ErrorLocation_12152.v
-	rw-r--r--	208	ErrorLocation_12255.out
-	rw-r--r--	125	ErrorLocation_12255.v
-	rw-r--r--	503	ErrorLocation_12774.out
-	rw-r--r--	105	ErrorLocation_12774.v
-	rw-r--r--	291	ErrorLocation_13241.out
-	rw-r--r--	174	ErrorLocation_13241.v
-	rw-r--r--	538	ErrorLocation_ltac.out
-	rw-r--r--	139	ErrorLocation_ltac.v
-	rw-r--r--	1,113	ErrorLocation_tac_in_term.out
-	rw-r--r--	352	ErrorLocation_tac_in_term.v
-	rw-r--r--	691	ErrorModuleWith.out
-	rw-r--r--	559	ErrorModuleWith.v
-	rw-r--r--	681	Error_msg_diffs.out
-	rw-r--r--	909	Error_msg_diffs.v
-	rw-r--r--	1,860	Errors.out
-	rw-r--r--	993	Errors.v
-	rw-r--r--	245	Existentials.out
-	rw-r--r--	242	Existentials.v
-	rw-r--r--	59	ExistingInstance.out
-	rw-r--r--	94	ExistingInstance.v
-	rw-r--r--	2,638	ExtractionString.out
-	rw-r--r--	599	ExtractionString.v
-	rw-r--r--	1,807	Extraction_Haskell_String_12258.out
-	rw-r--r--	1,854	Extraction_Haskell_String_12258.v
-	rw-r--r--	812	Extraction_ffi.out
-	rw-r--r--	996	Extraction_ffi.v
-	rw-r--r--	279	Extraction_infix.out
-	rw-r--r--	623	Extraction_infix.v
-	rw-r--r--	1,058	Extraction_matchs_2413.out
-	rw-r--r--	2,778	Extraction_matchs_2413.v
-	rw-r--r--	1,610	Fixpoint.out
-	rw-r--r--	2,154	Fixpoint.v
-	rw-r--r--	2,558	FloatExtraction.out
-	rw-r--r--	1,363	FloatExtraction.v
-	rw-r--r--	2,810	FloatNumberSyntax.out
-	rw-r--r--	954	FloatNumberSyntax.v
-	rw-r--r--	846	FunExt.out
-	rw-r--r--	4,819	FunExt.v
-	rw-r--r--	195	Function.out
-	rw-r--r--	1,070	Function.v
-	rw-r--r--	3,480	HintLocality.out
-	rw-r--r--	2,042	HintLocality.v
-	rw-r--r--	682	Implicit.out
-	rw-r--r--	1,852	Implicit.v
-	rw-r--r--	615	ImplicitTypes.out
-	rw-r--r--	1,059	ImplicitTypes.v
-	rw-r--r--	1,167	Inductive.out
-	rw-r--r--	700	Inductive.v
-	rw-r--r--	674	InductiveMainName.out
-	rw-r--r--	238	InductiveMainName.v
-	rw-r--r--	312	InitSyntax.out
-	rw-r--r--	111	InitSyntax.v
-	rw-r--r--	2,764	Int63NumberSyntax.out
-	rw-r--r--	1,142	Int63NumberSyntax.v
-	rw-r--r--	82	Intuition.out
-	rw-r--r--	121	Intuition.v
-	rw-r--r--	1,265	InvalidDisjunctiveIntro.out
-	rw-r--r--	888	InvalidDisjunctiveIntro.v
-	rw-r--r--	178	Load.out
-	rw-r--r--	130	Load.v
-	rw-r--r--	2,847	MExtraction.v
-	rw-r--r--	36	Match_subterm.out
-	rw-r--r--	93	Match_subterm.v
-	rw-r--r--	1,025	ModuleSubtyping.out
-	rw-r--r--	1,237	ModuleSubtyping.v
-	rw-r--r--	920	NNumberSyntax.out
-	rw-r--r--	964	NNumberSyntax.v
-	rw-r--r--	1,837	Nametab.out
-	rw-r--r--	1,062	Nametab.v
-	rw-r--r--	2,480	Naming.out
-	rw-r--r--	2,688	Naming.v
-	rw-r--r--	1,095	NatSyntax.out
-	rw-r--r--	296	NatSyntax.v
-	rw-r--r--	32	NoAxiomFromR.out
-	rw-r--r--	186	NoAxiomFromR.v
-	rw-r--r--	1,602	NotationSyntax.out
-	rw-r--r--	1,125	NotationSyntax.v
-	rw-r--r--	6,548	Notations.out
-	rw-r--r--	11,897	Notations.v
-	rw-r--r--	1,993	Notations2.out
-	rw-r--r--	4,923	Notations2.v
-	rw-r--r--	8,480	Notations3.out
-	rw-r--r--	18,188	Notations3.v
-	rw-r--r--	9,031	Notations4.out
-	rw-r--r--	17,347	Notations4.v
-	rw-r--r--	8,438	Notations5.out
-	rw-r--r--	8,236	Notations5.v
-	rw-r--r--	258	NotationsCoercions.out
-	rw-r--r--	2,064	NotationsCoercions.v
-	rw-r--r--	69	NotationsScope.out
-	rw-r--r--	390	NotationsScope.v
-	rw-r--r--	799	NotationsSigma.out
-	rw-r--r--	601	NotationsSigma.v
-	rw-r--r--	15,850	NumberNotations.out
-	rw-r--r--	30,756	NumberNotations.v
-	rw-r--r--	307	NumberNotationsUnivPoly.out
-	rw-r--r--	430	NumberNotationsUnivPoly.v
-	rw-r--r--	360	Partac.out
-	rw-r--r--	86	Partac.v
-	rw-r--r--	1,379	PatternsInBinders.out
-	rw-r--r--	1,795	PatternsInBinders.v
-	rw-r--r--	2,593	PosSyntax.out
-	rw-r--r--	1,249	PosSyntax.v
-	rw-r--r--	189	PrimStringSyntax.out
-	rw-r--r--	220	PrimStringSyntax.v
-	rw-r--r--	1,084	PrimitiveProjectionsAttribute.out
-	rw-r--r--	627	PrimitiveProjectionsAttribute.v
-	rw-r--r--	521	PrimitiveProjectionsAttribute_Records.out
-	rw-r--r--	390	PrimitiveProjectionsAttribute_Records.v
-	rw-r--r--	720	PrintAssumptions.out
-	rw-r--r--	4,481	PrintAssumptions.v
-	rw-r--r--	560	PrintCanonicalProjections.out
-	rw-r--r--	1,363	PrintCanonicalProjections.v
-	rw-r--r--	242	PrintGenarg.out
-	rw-r--r--	186	PrintGenarg.v
-	rw-r--r--	5,178	PrintGrammar.out
-	rw-r--r--	60	PrintGrammar.v
-	rw-r--r--	2,177	PrintGrammarConstr.out
-	rw-r--r--	152	PrintGrammarConstr.v
-	rw-r--r--	4,045	PrintInfos.out
-	rw-r--r--	1,271	PrintInfos.v
-	rw-r--r--	368	PrintKeywords.out
-	rw-r--r--	16	PrintKeywords.v
-	rw-r--r--	1,598	PrintMatch.out
-	rw-r--r--	563	PrintMatch.v
-	rw-r--r--	351	PrintModule.out
-	rw-r--r--	834	PrintModule.v
-	rw-r--r--	16,145	PrintNotation.out
-	rw-r--r--	6,010	PrintNotation.v
-	rw-r--r--	415	PrintPrimProj.out
-	rw-r--r--	737	PrintPrimProj.v
-	rw-r--r--	489	PrintSecDeps.out
-	rw-r--r--	185	PrintSecDeps.v
-	rw-r--r--	23	PrintUnivsSubgraph.out
-	rw-r--r--	200	PrintUnivsSubgraph.v
-	rw-r--r--	1,554	PrintingParentheses.out
-	rw-r--r--	769	PrintingParentheses.v
-	rw-r--r--	644	Projections.out
-	rw-r--r--	395	Projections.v
-	rw-r--r--	1,260	ProofUsingClashWarning.out
-	rw-r--r--	446	ProofUsingClashWarning.v
-	rw-r--r--	822	QArithSyntax.out
-	rw-r--r--	743	QArithSyntax.v
-	rw-r--r--	861	RealNumberSyntax.out
-	rw-r--r--	1,129	RealNumberSyntax.v
-	rw-r--r--	0	RecognizePluginWarning.out
-	rw-r--r--	280	RecognizePluginWarning.v
-	rw-r--r--	1,940	Record.out
-	rw-r--r--	2,255	Record.v
-	rw-r--r--	997	RecordFieldErrors.out
-	rw-r--r--	949	RecordFieldErrors.v
-	rw-r--r--	755	RecordMissingField.out
-	rw-r--r--	470	RecordMissingField.v
-	rw-r--r--	1,068	RecordProjParameter.out
-	rw-r--r--	329	RecordProjParameter.v
-	rw-r--r--	21,155	SchemeNames.out
-	rw-r--r--	7,031	SchemeNames.v
-	rw-r--r--	12,711	Search.out
-	rw-r--r--	1,387	Search.v
-	rw-r--r--	61	SearchFixpoint.out
-	rw-r--r--	536	SearchFixpoint.v
-	rw-r--r--	3,450	SearchPattern.out
-	rw-r--r--	1,003	SearchPattern.v
-	rw-r--r--	120	SearchRewrite.out
-	rw-r--r--	384	SearchRewrite.v
-	rw-r--r--	680	SearchScheme.out
-	rw-r--r--	58	SearchScheme.v
-	rw-r--r--	6,685	Search_2.out
-	rw-r--r--	298	Search_2.v
-	rw-r--r--	1,188	Search_3.out
-	rw-r--r--	736	Search_3.v
-	rw-r--r--	29	Search_bug13298.out
-	rw-r--r--	94	Search_bug13298.v
-	rw-r--r--	21	Search_bug17963.out
-	rw-r--r--	95	Search_bug17963.v
-	rw-r--r--	2,027	Search_headconcl.out
-	rw-r--r--	494	Search_headconcl.v
-	rw-r--r--	139	Show.out
-	rw-r--r--	265	Show.v
-	rw-r--r--	58	ShowMatch.out
-	rw-r--r--	356	ShowMatch.v
-	rw-r--r--	31	ShowProof.out
-	rw-r--r--	152	ShowProof.v
-	rw-r--r--	503	ShowUnivs.out
-	rw-r--r--	726	ShowUnivs.v
-	rw-r--r--	2,658	Sint63NumberSyntax.out
-	rw-r--r--	948	Sint63NumberSyntax.v
-	rw-r--r--	27	SortQuality.out
-	rw-r--r--	158	SortQuality.v
-	rw-r--r--	35,426	StringSyntax.out
-	rw-r--r--	2,423	StringSyntax.v
-	rw-r--r--	303	StringSyntaxPrimitive.out
-	rw-r--r--	5,066	StringSyntaxPrimitive.v
-	rw-r--r--	395	Succeed.out
-	rw-r--r--	93	Succeed.v
-	rw-r--r--	353	SuggestProofUsing.out
-	rw-r--r--	1,163	SuggestProofUsing.v
-	rw-r--r--	99	Sum.out
-	rw-r--r--	93	Sum.v
-	rw-r--r--	733	Tactics.out
-	rw-r--r--	1,123	Tactics.v
-	rw-r--r--	260	TermSyntax.out
-	rw-r--r--	322	TermSyntax.v
-	rw-r--r--	89	TranspModtype.out
-	rw-r--r--	385	TranspModtype.v
-	rw-r--r--	841	TypeclassDebug.out
-	rw-r--r--	244	TypeclassDebug.v
-	rw-r--r--	158	UnboundRef.out
-	rw-r--r--	83	UnboundRef.v
-	rw-r--r--	100	UnclosedBlocks.out
-	rw-r--r--	182	UnclosedBlocks.v
-	rw-r--r--	253	UnexpectedType.out
-	rw-r--r--	997	UnexpectedType.v
-	rw-r--r--	1,398	Unicode.out
-	rw-r--r--	981	Unicode.v
-	rw-r--r--	7,681	UnivBinders.out
-	rw-r--r--	5,476	UnivBinders.v
-	rw-r--r--	338	UpdateLoc.out
-	rw-r--r--	190	UpdateLoc.v
-	rw-r--r--	14	UsePluginWarning.out
-	rw-r--r--	131	UsePluginWarning.v
-	rw-r--r--	13	UselessSyndef.out
-	rw-r--r--	122	UselessSyndef.v
-	rw-r--r--	144	Utf8Impargs.out
-	rw-r--r--	252	Utf8Impargs.v
-	rw-r--r--	210	Warnings.out
-	rw-r--r--	187	Warnings.v
-	rw-r--r--	1,495	ZNumberSyntax.out
-	rw-r--r--	1,592	ZNumberSyntax.v
-	rw-r--r--	963	activation.out
-	rw-r--r--	1,307	activation.v
-	rw-r--r--	271	allBytes.out
-	rw-r--r--	5,146	allBytes.v
-	rw-r--r--	923	apply_with.out
-	rw-r--r--	380	apply_with.v
-	rw-r--r--	488	auto.out
-	rw-r--r--	185	auto.v
-	rw-r--r--	163	btauto_counterexample.out
-	rw-r--r--	216	btauto_counterexample.v
-	rw-r--r--	381	bug12442.out
-	rw-r--r--	162	bug12442.v
-	rw-r--r--	291	bug5778.out
-	rw-r--r--	144	bug5778.v
-	rw-r--r--	301	bug6404.out
-	rw-r--r--	156	bug6404.v
-	rw-r--r--	59	bug6821.out
-	rw-r--r--	258	bug6821.v
-	rw-r--r--	96	bug7191.out
-	rw-r--r--	105	bug7191.v
-	rw-r--r--	650	bug7348.out
-	rw-r--r--	513	bug7348.v
-	rw-r--r--	1,009	bug_10739.out
-	rw-r--r--	631	bug_10739.v
-	rw-r--r--	86	bug_10803.out
-	rw-r--r--	415	bug_10803.v
-	rw-r--r--	30	bug_10824.out
-	rw-r--r--	220	bug_10824.v
-	rw-r--r--	14	bug_11342.out
-	rw-r--r--	316	bug_11342.v
-	rw-r--r--	157	bug_11347.out
-	rw-r--r--	193	bug_11347.v
-	rw-r--r--	28	bug_11608.out
-	rw-r--r--	340	bug_11608.v
-	rw-r--r--	225	bug_11934.out
-	rw-r--r--	443	bug_11934.v
-	rw-r--r--	210	bug_12159.out
-	rw-r--r--	856	bug_12159.v
-	rw-r--r--	56	bug_12777.out
-	rw-r--r--	84	bug_12777.v
-	rw-r--r--	440	bug_12887.out
-	rw-r--r--	251	bug_12887.v
-	rw-r--r--	272	bug_12908.out
-	rw-r--r--	354	bug_12908.v
-	rw-r--r--	61	bug_13004.out
-	rw-r--r--	125	bug_13004.v
-	rw-r--r--	240	bug_13018.out
-	rw-r--r--	1,363	bug_13018.v
-	rw-r--r--	31	bug_13112.out
-	rw-r--r--	169	bug_13112.v
-	rw-r--r--	106	bug_13238.out
-	rw-r--r--	176	bug_13238.v
-	rw-r--r--	73	bug_13240.out
-	rw-r--r--	133	bug_13240.v
-	rw-r--r--	522	bug_13244.out
-	rw-r--r--	87	bug_13244.v
-	rw-r--r--	496	bug_13266.out
-	rw-r--r--	252	bug_13266.v
-	rw-r--r--	123	bug_13320.out
-	rw-r--r--	87	bug_13320.v
-	rw-r--r--	282	bug_13595.out
-	rw-r--r--	247	bug_13595.v
-	rw-r--r--	0	bug_13821_native_command_line_warn.out
-	rw-r--r--	158	bug_13821_native_command_line_warn.v
-	rw-r--r--	414	bug_13857.out
-	rw-r--r--	182	bug_13857.v
-	rw-r--r--	4,092	bug_13942.out
-	rw-r--r--	11,417	bug_13942.v
-	rw-r--r--	100	bug_14141.out
-	rw-r--r--	151	bug_14141.v
-	rw-r--r--	202	bug_14815.out
-	rw-r--r--	113	bug_14815.v
-	rw-r--r--	94	bug_14899.out
-	rw-r--r--	103	bug_14899.v
-	rw-r--r--	307	bug_15020.out
-	rw-r--r--	78	bug_15020.v
-	rw-r--r--	350	bug_15097.out
-	rw-r--r--	85	bug_15097.v
-	rw-r--r--	127	bug_15106.out
-	rw-r--r--	220	bug_15106.v
-	rw-r--r--	168	bug_15221.out
-	rw-r--r--	387	bug_15221.v
-	rw-r--r--	194	bug_15322.out
-	rw-r--r--	858	bug_15322.v
-	rw-r--r--	151	bug_15334.out
-	rw-r--r--	147	bug_15334.v
-	rw-r--r--	527	bug_15687.out
-	rw-r--r--	551	bug_15687.v
-	rw-r--r--	35	bug_15709.out
-	rw-r--r--	88	bug_15709.v
-	rw-r--r--	489	bug_16219.out
-	rw-r--r--	396	bug_16219.v
-	rw-r--r--	185	bug_16224.out
-	rw-r--r--	248	bug_16224.v
-	rw-r--r--	266	bug_16262.out
-	rw-r--r--	360	bug_16262.v
-	rw-r--r--	92	bug_16335.out
-	rw-r--r--	24	bug_16335.v
-	rw-r--r--	51	bug_16411.out
-	rw-r--r--	158	bug_16411.v
-	rw-r--r--	28	bug_16558.out
-	rw-r--r--	62	bug_16558.v
-	rw-r--r--	21	bug_16562.out
-	rw-r--r--	58	bug_16562.v
-	rw-r--r--	42	bug_16565.out
-	rw-r--r--	75	bug_16565.v
-	rw-r--r--	60	bug_16566.out
-	rw-r--r--	72	bug_16566.v
-	rw-r--r--	35	bug_16596.out
-	rw-r--r--	45	bug_16596.v
-	rw-r--r--	162	bug_16613.out
-	rw-r--r--	72	bug_16613.v
-	rw-r--r--	146	bug_16716.out
-	rw-r--r--	307	bug_16716.v
-	rw-r--r--	320	bug_16816.out
-	rw-r--r--	152	bug_16816.v
-	rw-r--r--	634	bug_17002.out
-	rw-r--r--	307	bug_17002.v
-	rw-r--r--	454	bug_17155.out
-	rw-r--r--	304	bug_17155.v
-	rw-r--r--	133	bug_17369.out
-	rw-r--r--	350	bug_17369.v
-	rw-r--r--	159	bug_17372.out
-	rw-r--r--	48	bug_17372.v
-	rw-r--r--	66	bug_17386.out
-	rw-r--r--	137	bug_17386.v
-	rw-r--r--	277	bug_17579.out
-	rw-r--r--	207	bug_17579.v
-	rw-r--r--	1,261	bug_17594.out
-	rw-r--r--	1,102	bug_17594.v
-	rw-r--r--	18	bug_17627.out
-	rw-r--r--	92	bug_17627.v
-	rw-r--r--	213	bug_17708.out
-	rw-r--r--	71	bug_17708.v
-	rw-r--r--	26	bug_17829.out
-	rw-r--r--	104	bug_17829.v
-	rw-r--r--	448	bug_17854.out
-	rw-r--r--	631	bug_17854.v
-	rw-r--r--	137	bug_18138.out
-	rw-r--r--	265	bug_18138.v
-	rw-r--r--	96	bug_18223.out
-	rw-r--r--	605	bug_18223.v
-	rw-r--r--	180	bug_18342.out
-	rw-r--r--	1,240	bug_18342.v
-	rw-r--r--	2	bug_18368.out
-	rw-r--r--	125	bug_18368.v
-	rw-r--r--	214	bug_18657.out
-	rw-r--r--	1,012	bug_18657.v
-	rw-r--r--	25	bug_18914.out
-	rw-r--r--	396	bug_18914.v
-	rw-r--r--	758	bug_19047.out
-	rw-r--r--	646	bug_19047.v
-	rw-r--r--	66	bug_19138.out
-	rw-r--r--	554	bug_19138.v
-	rw-r--r--	0	bug_19541.out
-	rw-r--r--	131	bug_19541.v
-	rw-r--r--	0	bug_19658.out
-	rw-r--r--	199	bug_19658.v
-	rw-r--r--	503	bug_19702.out
-	rw-r--r--	570	bug_19702.v
-	rw-r--r--	290	bug_19861.out
-	rw-r--r--	225	bug_19861.v
-	rw-r--r--	18	bug_20020.out
-	rw-r--r--	347	bug_20020.v
-	rw-r--r--	155	bug_3810.out
-	rw-r--r--	217	bug_3810.v
-	rw-r--r--	54	bug_4167.out
-	rw-r--r--	210	bug_4167.v
-	rw-r--r--	235	bug_4337.out
-	rw-r--r--	111	bug_4337.v
-	rw-r--r--	298	bug_4712_part2.out
-	rw-r--r--	205	bug_4712_part2.v
-	rw-r--r--	288	bug_5222.out
-	rw-r--r--	433	bug_5222.v
-	rw-r--r--	152	bug_6764.out
-	rw-r--r--	601	bug_6764.v
-	rw-r--r--	748	bug_7443.out
-	rw-r--r--	1,698	bug_7443.v
-	rw-r--r--	307	bug_8206.out
-	rw-r--r--	268	bug_8206.v
-	rw-r--r--	103	bug_9180.out
-	rw-r--r--	296	bug_9180.v
-	rw-r--r--	147	bug_9370.out
-	rw-r--r--	159	bug_9370.v
-	rw-r--r--	154	bug_9403.out
-	rw-r--r--	3,401	bug_9403.v
-	rw-r--r--	74	bug_9555.out
-	rw-r--r--	100	bug_9555.v
-	rw-r--r--	362	bug_9569.out
-	rw-r--r--	546	bug_9569.v
-	rw-r--r--	112	bug_9682.out
-	rw-r--r--	1,381	bug_9682.v
-	rw-r--r--	63	clear.out
-	rw-r--r--	241	clear.v
-	rw-r--r--	98	coercions_cs.out
-	rw-r--r--	541	coercions_cs.v
-	rw-r--r--	339	coercions_nonuniform.out
-	rw-r--r--	1,474	coercions_nonuniform.v
-	rw-r--r--	182	coercions_tc.out
-	rw-r--r--	680	coercions_tc.v
-	rw-r--r--	1,617	deprecation_definition.out
-	rw-r--r--	733	deprecation_definition.v
-	rw-r--r--	197	detype_cast.out
-	rw-r--r--	115	detype_cast.v
-	rw-r--r--	270	extra_dep.out
-	rw-r--r--	106	extra_dep.v
-	rw-r--r--	5,344	extraction_projection.out
-	rw-r--r--	3,143	extraction_projection.v
-	rw-r--r--	1,087	goal_output.out
-	rw-r--r--	573	goal_output.v
-	rw-r--r--	85	idtac.out
-	rw-r--r--	997	idtac.v
-	rw-r--r--	452	inference.out
-	rw-r--r--	727	inference.v
-	rw-r--r--	248	injection.out
-	rw-r--r--	211	injection.v
-	rw-r--r--	155	interleave_options_bad_order.out
-	rw-r--r--	100	interleave_options_bad_order.v
-	rw-r--r--	27	interleave_options_correct_order.out
-	rw-r--r--	100	interleave_options_correct_order.v
-	rw-r--r--	361	lexical_convention_in_doc.out
-	rw-r--r--	1,545	lexical_convention_in_doc.v
-	rw-r--r--	677	library_attributes.out
-	rw-r--r--	552	library_attributes.v
-	rw-r--r--	703	library_attributes_require.out
-	rw-r--r--	38	library_attributes_require.v
-	rw-r--r--	736	library_attributes_require_transitive.out
-	rw-r--r--	290	library_attributes_require_transitive.v
-	rw-r--r--	808	library_attributes_require_transitive_2.out
-	rw-r--r--	267	library_attributes_require_transitive_2.v
-	rw-r--r--	610	locate.out
-	rw-r--r--	464	locate.v
-	rw-r--r--	2,075	ltac.out
-	rw-r--r--	1,732	ltac.v
-	rw-r--r--	1,949	ltac2_abstract.out
-	rw-r--r--	2,040	ltac2_abstract.v
-	rw-r--r--	247	ltac2_anomaly_backtrace.out
-	rw-r--r--	581	ltac2_anomaly_backtrace.v
-	rw-r--r--	976	ltac2_bt.out
-	rw-r--r--	357	ltac2_bt.v
-	rw-r--r--	1,145	ltac2_check_globalize.out
-	rw-r--r--	1,090	ltac2_check_globalize.v
-	rw-r--r--	561	ltac2_deprecated.out
-	rw-r--r--	356	ltac2_deprecated.v
-	rw-r--r--	416	ltac2_match.out
-	rw-r--r--	1,424	ltac2_match.v
-	rw-r--r--	647	ltac2_notations_eval_in.out
-	rw-r--r--	1,065	ltac2_notations_eval_in.v
-	rw-r--r--	61	ltac2_pr_ctor.out
-	rw-r--r--	328	ltac2_pr_ctor.v
-	rw-r--r--	936	ltac2_printabout.out
-	rw-r--r--	1,047	ltac2_printabout.v
-	rw-r--r--	504	ltac2_typed_notations.out
-	rw-r--r--	299	ltac2_typed_notations.v
-	rw-r--r--	1,687	ltac2_unused_var.out
-	rw-r--r--	1,261	ltac2_unused_var.v
-	rw-r--r--	618	ltac_extra_args.out
-	rw-r--r--	135	ltac_extra_args.v
-	rw-r--r--	2,741	ltac_missing_args.out
-	rw-r--r--	405	ltac_missing_args.v
-	rw-r--r--	323	names.out
-	rw-r--r--	235	names.v
-	rw-r--r--	427	non_reversible_notation.out
-	rw-r--r--	125	non_reversible_notation.v
-	rw-r--r--	622	notation_prefix_incompatible_level.out
-	rw-r--r--	261	notation_prefix_incompatible_level.v
-	rw-r--r--	316	notation_previous_prefix.out
-	rw-r--r--	406	notation_previous_prefix.v
-	rw-r--r--	1,379	notation_principal_scope.out
-	rw-r--r--	630	notation_principal_scope.v
-	rw-r--r--	658	onlyprinting.out
-	rw-r--r--	690	onlyprinting.v
-	rw-r--r--	96	optimize_heap.out
-	rw-r--r--	115	optimize_heap.v
-	rw-r--r--	242	prim_array.out
-	rw-r--r--	153	prim_array.v
-	rw-r--r--	1,397	primitive_tokens.out
-	rw-r--r--	459	primitive_tokens.v
-	rw-r--r--	3,416	print_ltac.out
-	rw-r--r--	2,350	print_ltac.v
-	rw-r--r--	257	qualification.out
-	rw-r--r--	370	qualification.v
-	rw-r--r--	1,223	reduction.out
-	rw-r--r--	1,496	reduction.v
-	rw-r--r--	3,136	relaxed_ambiguous_paths.out
-	rw-r--r--	3,768	relaxed_ambiguous_paths.v
-	rw-r--r--	104	reverse_coercions.out
-	rw-r--r--	211	reverse_coercions.v
-	rw-r--r--	149	rewrite_2172.out
-	rw-r--r--	741	rewrite_2172.v
-	rw-r--r--	1,160	rewrite_strat.out
-	rw-r--r--	1,354	rewrite_strat.v
-	rw-r--r--	130	section_have.out
-	rw-r--r--	169	section_have.v
-	rw-r--r--	267	set.out
-	rw-r--r--	154	set.v
-	rw-r--r--	0	signatureT.out
-	rw-r--r--	43	signatureT.v
-	rw-r--r--	5,942	simpl.out
-	rw-r--r--	11,955	simpl.v
-	rw-r--r--	374	sint63NumberNotation.out
-	rw-r--r--	1,023	sint63NumberNotation.v
-	rw-r--r--	352	smartlocate.out
-	rw-r--r--	45	smartlocate.v
-	rw-r--r--	1,640	sort_poly_elim_error.out
-	rw-r--r--	929	sort_poly_elim_error.v
-	rw-r--r--	134	ssr_clear.out
-	rw-r--r--	97	ssr_clear.v
-	rw-r--r--	139	ssr_error_multiple_intro_after_case.out
-	rw-r--r--	85	ssr_error_multiple_intro_after_case.v
-	rw-r--r--	2,524	ssr_explain_match.out
-	rw-r--r--	1,033	ssr_explain_match.v
-	rw-r--r--	135	ssr_pred.out
-	rw-r--r--	55	ssr_pred.v
-	rw-r--r--	126	ssr_under.out
-	rw-r--r--	806	ssr_under.v
-	rw-r--r--	613	subst.out
-	rw-r--r--	985	subst.v
-	rw-r--r--	1,016	undeclared_key.out
-	rw-r--r--	206	undeclared_key.v
-	rw-r--r--	1,930	unifconstraints.out
-	rw-r--r--	1,119	unifconstraints.v
-	rw-r--r--	1,082	unification.out
-	rw-r--r--	949	unification.v
-	rw-r--r--	117	wish_17316.out
-	rw-r--r--	81	wish_17316.v
-	rw-r--r--	151	wish_17985.out
-	rw-r--r--	137	wish_17985.v
-	rw-r--r--	413	wish_18097.out
-	rw-r--r--	47	wish_18097.v