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

Mode	Name	Size
-rw-r--r--	Arguments.out	4240	log plain
-rw-r--r--	Arguments.v	1753	log plain
-rw-r--r--	ArgumentsScope.out	1605	log plain
-rw-r--r--	ArgumentsScope.v	607	log plain
-rw-r--r--	Arguments_renaming.out	4526	log plain
-rw-r--r--	Arguments_renaming.v	1100	log plain
-rw-r--r--	BadOptionValueType.out	417	log plain
-rw-r--r--	BadOptionValueType.v	113	log plain
-rw-r--r--	Binder.out	168	log plain
-rw-r--r--	Binder.v	134	log plain
-rw-r--r--	Cases.out	4580	log plain
-rw-r--r--	Cases.v	6526	log plain
-rw-r--r--	Coercions.out	108	log plain
-rw-r--r--	Coercions.v	697	log plain
-rw-r--r--	CompactContexts.out	142	log plain
-rw-r--r--	CompactContexts.v	141	log plain
-rw-r--r--	Deprecation.out	133	log plain
-rw-r--r--	Deprecation.v	102	log plain
-rw-r--r--	ErrorInCanonicalStructures.out	139	log plain
-rw-r--r--	ErrorInCanonicalStructures.v	85	log plain
-rw-r--r--	ErrorInCanonicalStructures2.out	139	log plain
-rw-r--r--	ErrorInCanonicalStructures2.v	48	log plain
-rw-r--r--	ErrorInModule.out	116	log plain
-rw-r--r--	ErrorInModule.v	101	log plain
-rw-r--r--	ErrorInSection.out	116	log plain
-rw-r--r--	ErrorInSection.v	102	log plain
-rw-r--r--	Error_msg_diffs.out	638	log plain
-rw-r--r--	Error_msg_diffs.v	904	log plain
-rw-r--r--	Errors.out	887	log plain
-rw-r--r--	Errors.v	785	log plain
-rw-r--r--	Existentials.out	245	log plain
-rw-r--r--	Existentials.v	242	log plain
-rw-r--r--	Extraction_infix.out	279	log plain
-rw-r--r--	Extraction_infix.v	623	log plain
-rw-r--r--	Extraction_matchs_2413.out	1058	log plain
-rw-r--r--	Extraction_matchs_2413.v	2801	log plain
-rw-r--r--	Fixpoint.out	519	log plain
-rw-r--r--	Fixpoint.v	1200	log plain
-rw-r--r--	FunExt.out	532	log plain
-rw-r--r--	FunExt.v	4819	log plain
-rw-r--r--	Implicit.out	391	log plain
-rw-r--r--	Implicit.v	1265	log plain
-rw-r--r--	Inductive.out	303	log plain
-rw-r--r--	Inductive.v	211	log plain
-rw-r--r--	InitSyntax.out	433	log plain
-rw-r--r--	InitSyntax.v	111	log plain
-rw-r--r--	Int31Syntax.out	252	log plain
-rw-r--r--	Int31Syntax.v	453	log plain
-rw-r--r--	Int63Syntax.out	450	log plain
-rw-r--r--	Int63Syntax.v	515	log plain
-rw-r--r--	Intuition.out	85	log plain
-rw-r--r--	Intuition.v	121	log plain
-rw-r--r--	InvalidDisjunctiveIntro.out	769	log plain
-rw-r--r--	InvalidDisjunctiveIntro.v	888	log plain
-rw-r--r--	Load.out	129	log plain
-rw-r--r--	Load.v	130	log plain
-rw-r--r--	MExtraction.v	577	log plain
-rw-r--r--	Match_subterm.out	36	log plain
-rw-r--r--	Match_subterm.v	93	log plain
-rw-r--r--	Nametab.out	1790	log plain
-rw-r--r--	Nametab.v	989	log plain
-rw-r--r--	Naming.out	1639	log plain
-rw-r--r--	Naming.v	1964	log plain
-rw-r--r--	Notations.out	3524	log plain
-rw-r--r--	Notations.v	8882	log plain
-rw-r--r--	Notations2.out	1993	log plain
-rw-r--r--	Notations2.v	4917	log plain
-rw-r--r--	Notations3.out	7868	log plain
-rw-r--r--	Notations3.v	14654	log plain
-rw-r--r--	Notations4.out	1599	log plain
-rw-r--r--	Notations4.v	3428	log plain
-rw-r--r--	NumeralNotations.out	5286	log plain
-rw-r--r--	NumeralNotations.v	14460	log plain
-rw-r--r--	PatternsInBinders.out	1346	log plain
-rw-r--r--	PatternsInBinders.v	1818	log plain
-rw-r--r--	PrintAssumptions.out	702	log plain
-rw-r--r--	PrintAssumptions.v	3543	log plain
-rw-r--r--	PrintInfos.out	3549	log plain
-rw-r--r--	PrintInfos.v	988	log plain
-rw-r--r--	PrintModule.out	216	log plain
-rw-r--r--	PrintModule.v	747	log plain
-rw-r--r--	PrintUnivsSubgraph.out	34	log plain
-rw-r--r--	PrintUnivsSubgraph.v	200	log plain
-rw-r--r--	Projections.out	59	log plain
-rw-r--r--	Projections.v	267	log plain
-rw-r--r--	RealSyntax.out	31	log plain
-rw-r--r--	RealSyntax.v	62	log plain
-rw-r--r--	RecognizePluginWarning.out	0	log plain
-rw-r--r--	RecognizePluginWarning.v	280	log plain
-rw-r--r--	Record.out	628	log plain
-rw-r--r--	Record.v	868	log plain
-rw-r--r--	RecordFieldErrors.out	564	log plain
-rw-r--r--	RecordFieldErrors.v	964	log plain
-rw-r--r--	RecordMissingField.out	116	log plain
-rw-r--r--	RecordMissingField.v	270	log plain
-rw-r--r--	Search.out	5213	log plain
-rw-r--r--	Search.v	1253	log plain
-rw-r--r--	SearchHead.out	1411	log plain
-rw-r--r--	SearchHead.v	460	log plain
-rw-r--r--	SearchPattern.out	2587	log plain
-rw-r--r--	SearchPattern.v	1003	log plain
-rw-r--r--	SearchRewrite.out	120	log plain
-rw-r--r--	SearchRewrite.v	384	log plain
-rw-r--r--	Show.out	148	log plain
-rw-r--r--	Show.v	265	log plain
-rw-r--r--	ShowMatch.out	58	log plain
-rw-r--r--	ShowMatch.v	402	log plain
-rw-r--r--	ShowProof.out	31	log plain
-rw-r--r--	ShowProof.v	152	log plain
-rw-r--r--	StringSyntax.out	33003	log plain
-rw-r--r--	StringSyntax.v	1133	log plain
-rw-r--r--	SuggestProofUsing.out	222	log plain
-rw-r--r--	SuggestProofUsing.v	547	log plain
-rw-r--r--	Sum.out	99	log plain
-rw-r--r--	Sum.v	93	log plain
-rw-r--r--	Tactics.out	256	log plain
-rw-r--r--	Tactics.v	569	log plain
-rw-r--r--	TranspModtype.out	89	log plain
-rw-r--r--	TranspModtype.v	385	log plain
-rw-r--r--	TypeclassDebug.out	782	log plain
-rw-r--r--	TypeclassDebug.v	234	log plain
-rw-r--r--	UnclosedBlocks.out	75	log plain
-rw-r--r--	UnclosedBlocks.v	182	log plain
-rw-r--r--	Unicode.out	1410	log plain
-rw-r--r--	Unicode.v	981	log plain
-rw-r--r--	UnivBinders.out	4894	log plain
-rw-r--r--	UnivBinders.v	4137	log plain
-rw-r--r--	UsePluginWarning.out	14	log plain
-rw-r--r--	UsePluginWarning.v	131	log plain
-rw-r--r--	Warnings.out	187	log plain
-rw-r--r--	Warnings.v	200	log plain
-rw-r--r--	ZSyntax.out	578	log plain
-rw-r--r--	ZSyntax.v	558	log plain
-rw-r--r--	auto.out	544	log plain
-rw-r--r--	auto.v	169	log plain
-rw-r--r--	bug5778.out	238	log plain
-rw-r--r--	bug5778.v	144	log plain
-rw-r--r--	bug6404.out	248	log plain
-rw-r--r--	bug6404.v	156	log plain
-rw-r--r--	bug6821.out	59	log plain
-rw-r--r--	bug6821.v	258	log plain
-rw-r--r--	bug_9180.out	101	log plain
-rw-r--r--	bug_9180.v	296	log plain
-rw-r--r--	bug_9370.out	156	log plain
-rw-r--r--	bug_9370.v	159	log plain
-rw-r--r--	goal_output.out	98	log plain
-rw-r--r--	goal_output.v	205	log plain
-rw-r--r--	idtac.out	85	log plain
-rw-r--r--	idtac.v	997	log plain
-rw-r--r--	inference.out	438	log plain
-rw-r--r--	inference.v	757	log plain
-rw-r--r--	injection.out	138	log plain
-rw-r--r--	injection.v	211	log plain
d---------	load	126	log plain
-rw-r--r--	ltac.out	1730	log plain
-rw-r--r--	ltac.v	1732	log plain
-rw-r--r--	ltac_extra_args.out	378	log plain
-rw-r--r--	ltac_extra_args.v	135	log plain
-rw-r--r--	ltac_missing_args.out	1785	log plain
-rw-r--r--	ltac_missing_args.v	405	log plain
-rw-r--r--	names.out	275	log plain
-rw-r--r--	names.v	235	log plain
-rw-r--r--	onlyprinting.out	18	log plain
-rw-r--r--	onlyprinting.v	107	log plain
-rw-r--r--	optimize_heap.out	102	log plain
-rw-r--r--	optimize_heap.v	115	log plain
-rw-r--r--	qualification.out	213	log plain
-rw-r--r--	qualification.v	370	log plain
-rw-r--r--	reduction.out	44	log plain
-rw-r--r--	reduction.v	279	log plain
-rw-r--r--	relaxed_ambiguous_paths.out	736	log plain
-rw-r--r--	relaxed_ambiguous_paths.v	1982	log plain
-rw-r--r--	rewrite_2172.out	91	log plain
-rw-r--r--	rewrite_2172.v	741	log plain
-rw-r--r--	set.out	276	log plain
-rw-r--r--	set.v	154	log plain
-rw-r--r--	simpl.out	198	log plain
-rw-r--r--	simpl.v	155	log plain
-rw-r--r--	sint63Notation.out	374	log plain
-rw-r--r--	sint63Notation.v	1024	log plain
-rw-r--r--	ssr_clear.out	80	log plain
-rw-r--r--	ssr_clear.v	97	log plain
-rw-r--r--	ssr_explain_match.out	2120	log plain
-rw-r--r--	ssr_explain_match.v	1033	log plain
-rw-r--r--	ssr_under.out	126	log plain
-rw-r--r--	ssr_under.v	806	log plain
-rw-r--r--	subst.out	1242	log plain
-rw-r--r--	subst.v	1588	log plain
-rw-r--r--	unifconstraints.out	1730	log plain
-rw-r--r--	unifconstraints.v	907	log plain