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

Mode	Name	Size
-rw-r--r--	Arguments.out	4136	log plain
-rw-r--r--	Arguments.v	1753	log plain
-rw-r--r--	ArgumentsScope.out	1587	log plain
-rw-r--r--	ArgumentsScope.v	607	log plain
-rw-r--r--	Arguments_renaming.out	3954	log plain
-rw-r--r--	Arguments_renaming.v	1091	log plain
-rw-r--r--	BadOptionValueType.out	654	log plain
-rw-r--r--	BadOptionValueType.v	183	log plain
-rw-r--r--	Binder.out	168	log plain
-rw-r--r--	Binder.v	134	log plain
-rw-r--r--	Cases.out	7349	log plain
-rw-r--r--	Cases.v	8145	log plain
-rw-r--r--	Coercions.out	108	log plain
-rw-r--r--	Coercions.v	651	log plain
-rw-r--r--	CompactContexts.out	139	log plain
-rw-r--r--	CompactContexts.v	141	log plain
-rw-r--r--	DebugFlags.out	1338	log plain
-rw-r--r--	DebugFlags.v	55	log plain
-rw-r--r--	DependentInductionErrors.out	270	log plain
-rw-r--r--	DependentInductionErrors.v	379	log plain
-rw-r--r--	Deprecation.out	133	log plain
-rw-r--r--	Deprecation.v	102	log plain
-rw-r--r--	Emacs_and_diffs.out	0	log plain
-rw-r--r--	Emacs_and_diffs.v	100	log plain
-rw-r--r--	EqNotation.out	111	log plain
-rw-r--r--	EqNotation.v	83	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	99	log plain
-rw-r--r--	ErrorInSection.out	116	log plain
-rw-r--r--	ErrorInSection.v	100	log plain
-rw-r--r--	ErrorLocation_12152_1.out	84	log plain
-rw-r--r--	ErrorLocation_12152_1.v	58	log plain
-rw-r--r--	ErrorLocation_12152_2.out	84	log plain
-rw-r--r--	ErrorLocation_12152_2.v	59	log plain
-rw-r--r--	ErrorLocation_12255.out	132	log plain
-rw-r--r--	ErrorLocation_12255.v	120	log plain
-rw-r--r--	ErrorLocation_12774_1.out	118	log plain
-rw-r--r--	ErrorLocation_12774_1.v	34	log plain
-rw-r--r--	ErrorLocation_12774_2.out	117	log plain
-rw-r--r--	ErrorLocation_12774_2.v	47	log plain
-rw-r--r--	ErrorLocation_12774_3.out	84	log plain
-rw-r--r--	ErrorLocation_12774_3.v	45	log plain
-rw-r--r--	ErrorLocation_13241_1.out	84	log plain
-rw-r--r--	ErrorLocation_13241_1.v	51	log plain
-rw-r--r--	ErrorLocation_13241_2.out	84	log plain
-rw-r--r--	ErrorLocation_13241_2.v	56	log plain
-rw-r--r--	ErrorLocation_ltac_1.out	87	log plain
-rw-r--r--	ErrorLocation_ltac_1.v	32	log plain
-rw-r--r--	ErrorLocation_ltac_2.out	62	log plain
-rw-r--r--	ErrorLocation_ltac_2.v	45	log plain
-rw-r--r--	ErrorLocation_ltac_3.out	81	log plain
-rw-r--r--	ErrorLocation_ltac_3.v	54	log plain
-rw-r--r--	ErrorLocation_ltac_4.out	64	log plain
-rw-r--r--	ErrorLocation_ltac_4.v	44	log plain
-rw-r--r--	ErrorLocation_tac_in_term_1.out	121	log plain
-rw-r--r--	ErrorLocation_tac_in_term_1.v	47	log plain
-rw-r--r--	ErrorLocation_tac_in_term_2.out	121	log plain
-rw-r--r--	ErrorLocation_tac_in_term_2.v	69	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--	ExtractionString.out	2638	log plain
-rw-r--r--	ExtractionString.v	599	log plain
-rw-r--r--	Extraction_Haskell_String_12258.out	1661	log plain
-rw-r--r--	Extraction_Haskell_String_12258.v	1854	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	2778	log plain
-rw-r--r--	Fixpoint.out	1520	log plain
-rw-r--r--	Fixpoint.v	2154	log plain
-rw-r--r--	FloatExtraction.out	2442	log plain
-rw-r--r--	FloatExtraction.v	1363	log plain
-rw-r--r--	FloatSyntax.out	2113	log plain
-rw-r--r--	FloatSyntax.v	954	log plain
-rw-r--r--	FunExt.out	532	log plain
-rw-r--r--	FunExt.v	4819	log plain
-rw-r--r--	Function.out	0	log plain
-rw-r--r--	Function.v	993	log plain
-rw-r--r--	HintLocality.out	2445	log plain
-rw-r--r--	HintLocality.v	1411	log plain
-rw-r--r--	Implicit.out	680	log plain
-rw-r--r--	Implicit.v	1852	log plain
-rw-r--r--	ImplicitTypes.out	615	log plain
-rw-r--r--	ImplicitTypes.v	1059	log plain
-rw-r--r--	Inductive.out	316	log plain
-rw-r--r--	Inductive.v	421	log plain
-rw-r--r--	InitSyntax.out	312	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	1397	log plain
-rw-r--r--	Int63Syntax.v	1130	log plain
-rw-r--r--	Intuition.out	82	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	2847	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	2380	log plain
-rw-r--r--	Naming.v	2688	log plain
-rw-r--r--	NatSyntax.out	760	log plain
-rw-r--r--	NatSyntax.v	296	log plain
-rw-r--r--	NoAxiomFromR.out	32	log plain
-rw-r--r--	NoAxiomFromR.v	186	log plain
-rw-r--r--	Notations.out	5546	log plain
-rw-r--r--	Notations.v	11897	log plain
-rw-r--r--	Notations2.out	1993	log plain
-rw-r--r--	Notations2.v	4913	log plain
-rw-r--r--	Notations3.out	7733	log plain
-rw-r--r--	Notations3.v	14978	log plain
-rw-r--r--	Notations4.out	5938	log plain
-rw-r--r--	Notations4.v	12730	log plain
-rw-r--r--	Notations5.out	7631	log plain
-rw-r--r--	Notations5.v	7986	log plain
-rw-r--r--	NotationsCoercions.out	258	log plain
-rw-r--r--	NotationsCoercions.v	2064	log plain
-rw-r--r--	NotationsSigma.out	799	log plain
-rw-r--r--	NotationsSigma.v	601	log plain
-rw-r--r--	NumberNotations.out	12803	log plain
-rw-r--r--	NumberNotations.v	29003	log plain
-rw-r--r--	Partac.out	258	log plain
-rw-r--r--	Partac.v	86	log plain
-rw-r--r--	PatternsInBinders.out	1262	log plain
-rw-r--r--	PatternsInBinders.v	1795	log plain
-rw-r--r--	PrintAssumptions.out	720	log plain
-rw-r--r--	PrintAssumptions.v	4481	log plain
-rw-r--r--	PrintCanonicalProjections.out	560	log plain
-rw-r--r--	PrintCanonicalProjections.v	1363	log plain
-rw-r--r--	PrintInfos.out	2646	log plain
-rw-r--r--	PrintInfos.v	988	log plain
-rw-r--r--	PrintModule.out	356	log plain
-rw-r--r--	PrintModule.v	834	log plain
-rw-r--r--	PrintUnivsSubgraph.out	34	log plain
-rw-r--r--	PrintUnivsSubgraph.v	200	log plain
-rw-r--r--	PrintingParentheses.out	1020	log plain
-rw-r--r--	PrintingParentheses.v	147	log plain
-rw-r--r--	Projections.out	514	log plain
-rw-r--r--	Projections.v	395	log plain
-rw-r--r--	QArithSyntax.out	822	log plain
-rw-r--r--	QArithSyntax.v	743	log plain
-rw-r--r--	RealSyntax.out	861	log plain
-rw-r--r--	RealSyntax.v	1129	log plain
-rw-r--r--	RecognizePluginWarning.out	0	log plain
-rw-r--r--	RecognizePluginWarning.v	280	log plain
-rw-r--r--	Record.out	1726	log plain
-rw-r--r--	Record.v	1741	log plain
-rw-r--r--	RecordFieldErrors.out	549	log plain
-rw-r--r--	RecordFieldErrors.v	949	log plain
-rw-r--r--	RecordMissingField.out	628	log plain
-rw-r--r--	RecordMissingField.v	470	log plain
-rw-r--r--	RecordProjParameter.out	849	log plain
-rw-r--r--	RecordProjParameter.v	329	log plain
-rw-r--r--	Search.out	19773	log plain
-rw-r--r--	Search.v	2460	log plain
-rw-r--r--	SearchPattern.out	3440	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--	Search_bug13298.out	29	log plain
-rw-r--r--	Search_bug13298.v	94	log plain
-rw-r--r--	Search_headconcl.out	1962	log plain
-rw-r--r--	Search_headconcl.v	494	log plain
-rw-r--r--	Show.out	139	log plain
-rw-r--r--	Show.v	265	log plain
-rw-r--r--	ShowMatch.out	58	log plain
-rw-r--r--	ShowMatch.v	356	log plain
-rw-r--r--	ShowProof.out	31	log plain
-rw-r--r--	ShowProof.v	152	log plain
-rw-r--r--	Sint63Syntax.out	1282	log plain
-rw-r--r--	Sint63Syntax.v	948	log plain
-rw-r--r--	StringSyntax.out	33276	log plain
-rw-r--r--	StringSyntax.v	2423	log plain
-rw-r--r--	StringSyntaxPrimitive.out	300	log plain
-rw-r--r--	StringSyntaxPrimitive.v	4669	log plain
-rw-r--r--	SuggestProofUsing.out	353	log plain
-rw-r--r--	SuggestProofUsing.v	1135	log plain
-rw-r--r--	Sum.out	99	log plain
-rw-r--r--	Sum.v	93	log plain
-rw-r--r--	Tactics.out	398	log plain
-rw-r--r--	Tactics.v	1026	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	244	log plain
-rw-r--r--	UnboundRef.out	106	log plain
-rw-r--r--	UnboundRef.v	78	log plain
-rw-r--r--	UnclosedBlocks.out	75	log plain
-rw-r--r--	UnclosedBlocks.v	182	log plain
-rw-r--r--	Unicode.out	1398	log plain
-rw-r--r--	Unicode.v	981	log plain
-rw-r--r--	UnivBinders.out	4755	log plain
-rw-r--r--	UnivBinders.v	4653	log plain
-rw-r--r--	UsePluginWarning.out	14	log plain
-rw-r--r--	UsePluginWarning.v	131	log plain
-rw-r--r--	UselessSyndef.out	13	log plain
-rw-r--r--	UselessSyndef.v	122	log plain
-rw-r--r--	Warnings.out	187	log plain
-rw-r--r--	Warnings.v	177	log plain
-rw-r--r--	ZSyntax.out	669	log plain
-rw-r--r--	ZSyntax.v	783	log plain
-rw-r--r--	allBytes.out	95	log plain
-rw-r--r--	allBytes.v	5063	log plain
-rw-r--r--	attributes.out	503	log plain
-rw-r--r--	attributes.v	296	log plain
-rw-r--r--	auto.out	488	log plain
-rw-r--r--	auto.v	171	log plain
-rw-r--r--	bug12442.out	222	log plain
-rw-r--r--	bug12442.v	162	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--	bug7191.out	96	log plain
-rw-r--r--	bug7191.v	105	log plain
-rw-r--r--	bug7348.out	650	log plain
-rw-r--r--	bug7348.v	513	log plain
-rw-r--r--	bug_10803.out	86	log plain
-rw-r--r--	bug_10803.v	415	log plain
-rw-r--r--	bug_10824.out	30	log plain
-rw-r--r--	bug_10824.v	220	log plain
-rw-r--r--	bug_11342.out	14	log plain
-rw-r--r--	bug_11342.v	316	log plain
-rw-r--r--	bug_11608.out	28	log plain
-rw-r--r--	bug_11608.v	340	log plain
-rw-r--r--	bug_11934.out	409	log plain
-rw-r--r--	bug_11934.v	443	log plain
-rw-r--r--	bug_12159.out	210	log plain
-rw-r--r--	bug_12159.v	855	log plain
-rw-r--r--	bug_12887.out	331	log plain
-rw-r--r--	bug_12887.v	251	log plain
-rw-r--r--	bug_12908.out	249	log plain
-rw-r--r--	bug_12908.v	354	log plain
-rw-r--r--	bug_13004.out	61	log plain
-rw-r--r--	bug_13004.v	125	log plain
-rw-r--r--	bug_13018.out	240	log plain
-rw-r--r--	bug_13018.v	1363	log plain
-rw-r--r--	bug_13112.out	31	log plain
-rw-r--r--	bug_13112.v	169	log plain
-rw-r--r--	bug_13238.out	106	log plain
-rw-r--r--	bug_13238.v	176	log plain
-rw-r--r--	bug_13240.out	73	log plain
-rw-r--r--	bug_13240.v	133	log plain
-rw-r--r--	bug_13244.out	522	log plain
-rw-r--r--	bug_13244.v	87	log plain
-rw-r--r--	bug_13266.out	441	log plain
-rw-r--r--	bug_13266.v	253	log plain
-rw-r--r--	bug_13320.out	69	log plain
-rw-r--r--	bug_13320.v	87	log plain
-rw-r--r--	bug_13595.out	228	log plain
-rw-r--r--	bug_13595.v	247	log plain
-rw-r--r--	bug_13821_native_command_line_warn.out	0	log plain
-rw-r--r--	bug_13821_native_command_line_warn.v	95	log plain
-rw-r--r--	bug_7443.out	228	log plain
-rw-r--r--	bug_7443.v	1698	log plain
-rw-r--r--	bug_8206.out	257	log plain
-rw-r--r--	bug_8206.v	263	log plain
-rw-r--r--	bug_9180.out	103	log plain
-rw-r--r--	bug_9180.v	296	log plain
-rw-r--r--	bug_9370.out	147	log plain
-rw-r--r--	bug_9370.v	159	log plain
-rw-r--r--	bug_9403.out	154	log plain
-rw-r--r--	bug_9403.v	3401	log plain
-rw-r--r--	bug_9569.out	362	log plain
-rw-r--r--	bug_9569.v	546	log plain
-rw-r--r--	bug_9682.out	112	log plain
-rw-r--r--	bug_9682.v	1381	log plain
-rw-r--r--	clear.out	63	log plain
-rw-r--r--	clear.v	241	log plain
-rw-r--r--	goal_output.out	1087	log plain
-rw-r--r--	goal_output.v	573	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	734	log plain
-rw-r--r--	injection.out	138	log plain
-rw-r--r--	injection.v	211	log plain
-rw-r--r--	interleave_options_bad_order.out	154	log plain
-rw-r--r--	interleave_options_bad_order.v	100	log plain
-rw-r--r--	interleave_options_correct_order.out	27	log plain
-rw-r--r--	interleave_options_correct_order.v	100	log plain
d---------	load	126	log plain
-rw-r--r--	locate.out	610	log plain
-rw-r--r--	locate.v	464	log plain
-rw-r--r--	ltac.out	1724	log plain
-rw-r--r--	ltac.v	1732	log plain
-rw-r--r--	ltac2_deprecated.out	471	log plain
-rw-r--r--	ltac2_deprecated.v	339	log plain
-rw-r--r--	ltac2_notations_eval_in.out	647	log plain
-rw-r--r--	ltac2_notations_eval_in.v	1065	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	272	log plain
-rw-r--r--	names.v	235	log plain
-rw-r--r--	notation_principal_scope.out	984	log plain
-rw-r--r--	notation_principal_scope.v	629	log plain
-rw-r--r--	onlyprinting.out	18	log plain
-rw-r--r--	onlyprinting.v	107	log plain
-rw-r--r--	optimize_heap.out	96	log plain
-rw-r--r--	optimize_heap.v	115	log plain
-rw-r--r--	prim_array.out	242	log plain
-rw-r--r--	prim_array.v	153	log plain
-rw-r--r--	primitive_tokens.out	1397	log plain
-rw-r--r--	primitive_tokens.v	459	log plain
-rw-r--r--	print_ltac.out	3302	log plain
-rw-r--r--	print_ltac.v	2350	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	2407	log plain
-rw-r--r--	relaxed_ambiguous_paths.v	3768	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	267	log plain
-rw-r--r--	set.v	154	log plain
-rw-r--r--	simpl.out	189	log plain
-rw-r--r--	simpl.v	155	log plain
-rw-r--r--	sint63Notation.out	374	log plain
-rw-r--r--	sint63Notation.v	1022	log plain
-rw-r--r--	ssr_clear.out	80	log plain
-rw-r--r--	ssr_clear.v	97	log plain
-rw-r--r--	ssr_error_multiple_intro_after_case.out	62	log plain
-rw-r--r--	ssr_error_multiple_intro_after_case.v	80	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_pred.out	135	log plain
-rw-r--r--	ssr_pred.v	55	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	1218	log plain
-rw-r--r--	subst.v	1588	log plain
-rw-r--r--	undeclared_key.out	700	log plain
-rw-r--r--	undeclared_key.v	206	log plain
-rw-r--r--	unifconstraints.out	1694	log plain
-rw-r--r--	unifconstraints.v	907	log plain
-rw-r--r--	unification.out	829	log plain
-rw-r--r--	unification.v	581	log plain