output « test-suite - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	Arguments.out	3463	log plain
-rw-r--r--	Arguments.v	1470	log plain
-rw-r--r--	ArgumentsScope.out	1083	log plain
-rw-r--r--	ArgumentsScope.v	560	log plain
-rw-r--r--	Arguments_renaming.out	4378	log plain
-rw-r--r--	Arguments_renaming.v	1049	log plain
-rw-r--r--	Binder.out	168	log plain
-rw-r--r--	Binder.v	134	log plain
-rw-r--r--	Cases.out	2014	log plain
-rw-r--r--	Cases.v	2420	log plain
-rw-r--r--	Coercions.out	108	log plain
-rw-r--r--	Coercions.v	651	log plain
-rw-r--r--	Errors.out	458	log plain
-rw-r--r--	Errors.v	548	log plain
-rw-r--r--	Existentials.out	237	log plain
-rw-r--r--	Existentials.v	225	log plain
-rw-r--r--	Extraction_matchs_2413.out	1058	log plain
-rw-r--r--	Extraction_matchs_2413.v	2742	log plain
-rw-r--r--	Fixpoint.out	519	log plain
-rw-r--r--	Fixpoint.v	1179	log plain
-rw-r--r--	FunExt.out	873	log plain
-rw-r--r--	FunExt.v	4767	log plain
-rw-r--r--	Implicit.out	391	log plain
-rw-r--r--	Implicit.v	1267	log plain
-rw-r--r--	Inductive.out	143	log plain
-rw-r--r--	Inductive.v	94	log plain
-rw-r--r--	InitSyntax.out	433	log plain
-rw-r--r--	InitSyntax.v	111	log plain
-rw-r--r--	Intuition.out	85	log plain
-rw-r--r--	Intuition.v	121	log plain
-rw-r--r--	Match_subterm.out	36	log plain
-rw-r--r--	Match_subterm.v	86	log plain
-rw-r--r--	Nametab.out	1672	log plain
-rw-r--r--	Nametab.v	917	log plain
-rw-r--r--	Naming.out	1639	log plain
-rw-r--r--	Naming.v	1957	log plain
-rw-r--r--	Notations.out	3661	log plain
-rw-r--r--	Notations.v	8482	log plain
-rw-r--r--	Notations2.out	1594	log plain
-rw-r--r--	Notations2.v	4183	log plain
-rw-r--r--	Notations3.out	3528	log plain
-rw-r--r--	Notations3.v	5247	log plain
-rw-r--r--	NumbersSyntax.out	950	log plain
-rw-r--r--	NumbersSyntax.v	1351	log plain
-rw-r--r--	PatternsInBinders.out	1168	log plain
-rw-r--r--	PatternsInBinders.v	1613	log plain
-rw-r--r--	PrintAssumptions.out	574	log plain
-rw-r--r--	PrintAssumptions.v	2582	log plain
-rw-r--r--	PrintInfos.out	3366	log plain
-rw-r--r--	PrintInfos.v	947	log plain
-rw-r--r--	PrintModule.out	146	log plain
-rw-r--r--	PrintModule.v	567	log plain
-rw-r--r--	Quote.out	963	log plain
-rw-r--r--	Quote.v	911	log plain
-rw-r--r--	RealSyntax.out	31	log plain
-rw-r--r--	RealSyntax.v	49	log plain
-rw-r--r--	Record.out	212	log plain
-rw-r--r--	Record.v	385	log plain
-rw-r--r--	Search.out	4123	log plain
-rw-r--r--	Search.v	1122	log plain
-rw-r--r--	SearchHead.out	1411	log plain
-rw-r--r--	SearchHead.v	460	log plain
-rw-r--r--	SearchPattern.out	2215	log plain
-rw-r--r--	SearchPattern.v	1002	log plain
-rw-r--r--	SearchRewrite.out	120	log plain
-rw-r--r--	SearchRewrite.v	384	log plain
-rw-r--r--	ShowProof.out	31	log plain
-rw-r--r--	ShowProof.v	145	log plain
-rw-r--r--	Sum.out	99	log plain
-rw-r--r--	Sum.v	93	log plain
-rw-r--r--	Tactics.out	130	log plain
-rw-r--r--	Tactics.v	357	log plain
-rw-r--r--	TranspModtype.out	89	log plain
-rw-r--r--	TranspModtype.v	385	log plain
-rw-r--r--	ZSyntax.out	578	log plain
-rw-r--r--	ZSyntax.v	558	log plain
-rw-r--r--	auto.out	505	log plain
-rw-r--r--	auto.v	138	log plain
-rw-r--r--	inference.out	563	log plain
-rw-r--r--	inference.v	881	log plain
-rw-r--r--	ltac.out	1370	log plain
-rw-r--r--	ltac.v	1261	log plain
-rw-r--r--	ltac_missing_args.out	1208	log plain
-rw-r--r--	ltac_missing_args.v	383	log plain
-rw-r--r--	names.out	168	log plain
-rw-r--r--	names.v	132	log plain
-rw-r--r--	onlyprinting.out	18	log plain
-rw-r--r--	onlyprinting.v	107	log plain
-rw-r--r--	qualification.out	172	log plain
-rw-r--r--	qualification.v	324	log plain
-rw-r--r--	reduction.out	44	log plain
-rw-r--r--	reduction.v	279	log plain
-rw-r--r--	rewrite-2172.out	91	log plain
-rw-r--r--	rewrite-2172.v	734	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	148	log plain
-rw-r--r--	subst.out	1242	log plain
-rw-r--r--	subst.v	1588	log plain
-rw-r--r--	unifconstraints.out	1487	log plain
-rw-r--r--	unifconstraints.v	655	log plain