closed « bugs « test-suite - coq - the Coq proof assistant

Mode	Name	Size
-rw-r--r--	1100.v	197	log plain
-rw-r--r--	121.v	420	log plain
-rw-r--r--	1243.v	195	log plain
-rw-r--r--	1302.v	259	log plain
-rw-r--r--	1322.v	567	log plain
-rw-r--r--	1411.v	922	log plain
-rw-r--r--	1414.v	1186	log plain
-rw-r--r--	1416.v	962	log plain
-rw-r--r--	1419.v	110	log plain
-rw-r--r--	1425.v	481	log plain
-rw-r--r--	1446.v	350	log plain
-rw-r--r--	1448.v	638	log plain
-rw-r--r--	1477.v	312	log plain
-rw-r--r--	1483.v	150	log plain
-rw-r--r--	1507.v	4534	log plain
-rw-r--r--	1519.v	310	log plain
-rw-r--r--	1568.v	185	log plain
-rw-r--r--	1576.v	468	log plain
-rw-r--r--	1582.v	242	log plain
-rw-r--r--	1604.v	171	log plain
-rw-r--r--	1614.v	487	log plain
-rw-r--r--	1618.v	408	log plain
-rw-r--r--	1634.v	631	log plain
-rw-r--r--	1643.v	475	log plain
-rw-r--r--	1680.v	190	log plain
-rw-r--r--	1683.v	995	log plain
-rw-r--r--	1696.v	432	log plain
-rw-r--r--	1703.v	196	log plain
-rw-r--r--	1704.v	389	log plain
-rw-r--r--	1711.v	1006	log plain
-rw-r--r--	1718.v	182	log plain
-rw-r--r--	1738.v	622	log plain
-rw-r--r--	1740.v	471	log plain
-rw-r--r--	1754.v	673	log plain
-rw-r--r--	1773.v	234	log plain
-rw-r--r--	1774.v	512	log plain
-rw-r--r--	1775.v	1016	log plain
-rw-r--r--	1776.v	620	log plain
-rw-r--r--	1779.v	836	log plain
-rw-r--r--	1780.v	291	log plain
-rw-r--r--	1784.v	2931	log plain
-rw-r--r--	1787.v	264	log plain
-rw-r--r--	1791.v	823	log plain
-rw-r--r--	1834.v	5043	log plain
-rw-r--r--	1844.v	7442	log plain
-rw-r--r--	1865.v	418	log plain
-rw-r--r--	1891.v	306	log plain
-rw-r--r--	1898.v	129	log plain
-rw-r--r--	1900.v	99	log plain
-rw-r--r--	1901.v	301	log plain
-rw-r--r--	1905.v	221	log plain
-rw-r--r--	1907.v	169	log plain
-rw-r--r--	1912.v	84	log plain
-rw-r--r--	1915.v	115	log plain
-rw-r--r--	1918.v	9247	log plain
-rw-r--r--	1925.v	731	log plain
-rw-r--r--	1931.v	610	log plain
-rw-r--r--	1935.v	362	log plain
-rw-r--r--	1939.v	356	log plain
-rw-r--r--	1944.v	224	log plain
-rw-r--r--	1951.v	1616	log plain
-rw-r--r--	1962.v	1415	log plain
-rw-r--r--	1963.v	550	log plain
-rw-r--r--	1977.v	76	log plain
-rw-r--r--	1981.v	103	log plain
-rw-r--r--	2001.v	355	log plain
-rw-r--r--	2006.v	598	log plain
-rw-r--r--	2017.v	488	log plain
-rw-r--r--	2021.v	571	log plain
-rw-r--r--	2027.v	226	log plain
-rw-r--r--	2080.v	43	log plain
-rw-r--r--	2083.v	683	log plain
-rw-r--r--	2089.v	599	log plain
-rw-r--r--	2095.v	312	log plain
-rw-r--r--	2105.v	49	log plain
-rw-r--r--	2108.v	407	log plain
-rw-r--r--	2117.v	2177	log plain
-rw-r--r--	2123.v	297	log plain
-rw-r--r--	2127.v	238	log plain
-rw-r--r--	2135.v	310	log plain
-rw-r--r--	2136.v	1494	log plain
-rw-r--r--	2137.v	1271	log plain
-rw-r--r--	2139.v	730	log plain
-rw-r--r--	2141.v	317	log plain
-rw-r--r--	2145.v	414	log plain
-rw-r--r--	2164.v	10782	log plain
-rw-r--r--	2181.v	74	log plain
-rw-r--r--	2193.v	1123	log plain
-rw-r--r--	2230.v	97	log plain
-rw-r--r--	2231.v	134	log plain
-rw-r--r--	2244.v	520	log plain
-rw-r--r--	2250.v	122	log plain
-rw-r--r--	2251.v	195	log plain
-rw-r--r--	2255.v	766	log plain
-rw-r--r--	2262.v	206	log plain
-rw-r--r--	2281.v	1204	log plain
-rw-r--r--	2295.v	270	log plain
-rw-r--r--	2299.v	220	log plain
-rw-r--r--	2300.v	247	log plain
-rw-r--r--	2303.v	139	log plain
-rw-r--r--	2304.v	145	log plain
-rw-r--r--	2307.v	102	log plain
-rw-r--r--	2310.v	637	log plain
-rw-r--r--	2319.v	299	log plain
-rw-r--r--	2320.v	564	log plain
-rw-r--r--	2342.v	237	log plain
-rw-r--r--	2347.v	352	log plain
-rw-r--r--	2350.v	187	log plain
-rw-r--r--	2353.v	496	log plain
-rw-r--r--	2360.v	367	log plain
-rw-r--r--	2362.v	860	log plain
-rw-r--r--	2375.v	354	log plain
-rw-r--r--	2378.v	21297	log plain
-rw-r--r--	2388.v	355	log plain
-rw-r--r--	2393.v	286	log plain
-rw-r--r--	2404.v	1422	log plain
-rw-r--r--	2406.v	212	log plain
-rw-r--r--	2456.v	1803	log plain
-rw-r--r--	2464.v	1239	log plain
-rw-r--r--	2467.v	1551	log plain
-rw-r--r--	2473.v	1068	log plain
-rw-r--r--	2586.v	134	log plain
-rw-r--r--	2603.v	891	log plain
-rw-r--r--	2608.v	948	log plain
-rw-r--r--	2613.v	392	log plain
-rw-r--r--	2615.v	613	log plain
-rw-r--r--	2616.v	203	log plain
-rw-r--r--	2629.v	729	log plain
-rw-r--r--	2640.v	329	log plain
-rw-r--r--	2667.v	445	log plain
-rw-r--r--	2668.v	169	log plain
-rw-r--r--	2670.v	778	log plain
-rw-r--r--	2680.v	281	log plain
-rw-r--r--	2729.v	3004	log plain
-rw-r--r--	2732.v	320	log plain
-rw-r--r--	2733.v	885	log plain
-rw-r--r--	2734.v	344	log plain
-rw-r--r--	2750.v	333	log plain
-rw-r--r--	2817.v	291	log plain
-rw-r--r--	2818.v	86	log plain
-rw-r--r--	2830.v	7790	log plain
-rw-r--r--	2834.v	106	log plain
-rw-r--r--	2836.v	1357	log plain
-rw-r--r--	2837.v	403	log plain
-rw-r--r--	2839.v	272	log plain
-rw-r--r--	2846.v	51	log plain
-rw-r--r--	2848.v	269	log plain
-rw-r--r--	2883.v	841	log plain
-rw-r--r--	2900.v	813	log plain
-rw-r--r--	2923.v	240	log plain
-rw-r--r--	2928.v	346	log plain
-rw-r--r--	2930.v	292	log plain
-rw-r--r--	2955.v	664	log plain
-rw-r--r--	2966.v	1879	log plain
-rw-r--r--	2969.v	537	log plain
-rw-r--r--	2981.v	702	log plain
-rw-r--r--	2983.v	127	log plain
-rw-r--r--	2990.v	121	log plain
-rw-r--r--	2994.v	75	log plain
-rw-r--r--	2995.v	241	log plain
-rw-r--r--	2996.v	576	log plain
-rw-r--r--	3000.v	112	log plain
-rw-r--r--	3001.v	769	log plain
-rw-r--r--	3003.v	524	log plain
-rw-r--r--	3004.v	246	log plain
-rw-r--r--	3008.v	664	log plain
-rw-r--r--	3010b.v	143	log plain
-rw-r--r--	3016.v	90	log plain
-rw-r--r--	3017.v	160	log plain
-rw-r--r--	3022.v	250	log plain
-rw-r--r--	3023.v	843	log plain
-rw-r--r--	3036.v	4805	log plain
-rw-r--r--	3037.v	322	log plain
-rw-r--r--	3043.v	148	log plain
-rw-r--r--	3050.v	116	log plain
-rw-r--r--	3054.v	81	log plain
-rw-r--r--	3062.v	105	log plain
-rw-r--r--	3088.v	372	log plain
-rw-r--r--	3093.v	126	log plain
-rw-r--r--	3142.v	377	log plain
-rw-r--r--	3164.v	1231	log plain
-rw-r--r--	3188.v	632	log plain
-rw-r--r--	3205.v	807	log plain
-rw-r--r--	3212.v	143	log plain
-rw-r--r--	3217.v	765	log plain
-rw-r--r--	3228.v	169	log plain
-rw-r--r--	3242.v	46	log plain
-rw-r--r--	3251.v	515	log plain
-rw-r--r--	3259.v	242	log plain
-rw-r--r--	3260.v	142	log plain
-rw-r--r--	3262.v	2700	log plain
-rw-r--r--	3264.v	946	log plain
-rw-r--r--	3265.v	236	log plain
-rw-r--r--	3266.v	74	log plain
-rw-r--r--	3267.v	839	log plain
-rw-r--r--	328.v	786	log plain
-rw-r--r--	3281.v	149	log plain
-rw-r--r--	3282.v	257	log plain
-rw-r--r--	3284.v	827	log plain
-rw-r--r--	3285.v	106	log plain
-rw-r--r--	3286.v	1595	log plain
-rw-r--r--	3287.v	308	log plain
-rw-r--r--	3289.v	829	log plain
-rw-r--r--	329.v	2353	log plain
-rw-r--r--	3291.v	348	log plain
-rw-r--r--	3294.v	204	log plain
-rw-r--r--	3297.v	328	log plain
-rw-r--r--	3300.v	214	log plain
-rw-r--r--	3305.v	264	log plain
-rw-r--r--	3306.v	281	log plain
-rw-r--r--	3309.v	11789	log plain
-rw-r--r--	331.v	262	log plain
-rw-r--r--	3310.v	297	log plain
-rw-r--r--	3314.v	3948	log plain
-rw-r--r--	3315.v	1175	log plain
-rw-r--r--	3317.v	3799	log plain
-rw-r--r--	3319.v	1049	log plain
-rw-r--r--	3321.v	1263	log plain
-rw-r--r--	3322.v	1211	log plain
-rw-r--r--	3323.v	4196	log plain
-rw-r--r--	3324.v	1890	log plain
-rw-r--r--	3325.v	1290	log plain
-rw-r--r--	3329.v	3911	log plain
-rw-r--r--	3330.v	28645	log plain
-rw-r--r--	3331.v	1557	log plain
-rw-r--r--	3332.v	259	log plain
-rw-r--r--	3336.v	229	log plain
-rw-r--r--	3337.v	102	log plain
-rw-r--r--	3338.v	111	log plain
-rw-r--r--	3344.v	2618	log plain
-rw-r--r--	3346.v	230	log plain
-rw-r--r--	3347.v	2176	log plain
-rw-r--r--	3348.v	247	log plain
-rw-r--r--	335.v	107	log plain
-rw-r--r--	3350.v	4148	log plain
-rw-r--r--	3352.v	4148	log plain
-rw-r--r--	3354.v	386	log plain
-rw-r--r--	3355.v	167	log plain
-rw-r--r--	3368.v	871	log plain
-rw-r--r--	3372.v	318	log plain
-rw-r--r--	3373.v	1348	log plain
-rw-r--r--	3374.v	2461	log plain
-rw-r--r--	3375.v	2800	log plain
-rw-r--r--	3377.v	444	log plain
-rw-r--r--	3382.v	3226	log plain
-rw-r--r--	3386.v	521	log plain
-rw-r--r--	3387.v	556	log plain
-rw-r--r--	3390.v	353	log plain
-rw-r--r--	3392.v	2371	log plain
-rw-r--r--	3393.v	6705	log plain
-rw-r--r--	3402.v	187	log plain
-rw-r--r--	3416.v	390	log plain
-rw-r--r--	3422.v	6795	log plain
-rw-r--r--	3427.v	8147	log plain
-rw-r--r--	3428.v	1401	log plain
-rw-r--r--	3439.v	1579	log plain
-rw-r--r--	3453.v	281	log plain
-rw-r--r--	3454.v	2468	log plain
-rw-r--r--	3469.v	974	log plain
-rw-r--r--	3477.v	294	log plain
-rw-r--r--	348.v	186	log plain
-rw-r--r--	3480.v	2153	log plain
-rw-r--r--	3481.v	1823	log plain
-rw-r--r--	3482.v	392	log plain
-rw-r--r--	3483.v	164	log plain
-rw-r--r--	3484.v	1202	log plain
-rw-r--r--	3505.v	1976	log plain
-rw-r--r--	3520.v	200	log plain
-rw-r--r--	3531.v	2370	log plain
-rw-r--r--	3537.v	314	log plain
-rw-r--r--	3539.v	3365	log plain
-rw-r--r--	3546.v	485	log plain
-rw-r--r--	3559.v	3492	log plain
-rw-r--r--	3561.v	1242	log plain
-rw-r--r--	3563.v	1802	log plain
-rw-r--r--	3566.v	1129	log plain
-rw-r--r--	3567.v	3272	log plain
-rw-r--r--	3584.v	720	log plain
-rw-r--r--	3593.v	360	log plain
-rw-r--r--	3594.v	2653	log plain
-rw-r--r--	3596.v	481	log plain
-rw-r--r--	3616.v	154	log plain
-rw-r--r--	3624.v	285	log plain
-rw-r--r--	3625.v	198	log plain
-rw-r--r--	3633.v	330	log plain
-rw-r--r--	3637.v	328	log plain
-rw-r--r--	3638.v	1360	log plain
-rw-r--r--	3641.v	1236	log plain
-rw-r--r--	3647.v	23010	log plain
-rw-r--r--	3648.v	3165	log plain
-rw-r--r--	3653.v	219	log plain
-rw-r--r--	3656.v	1464	log plain
-rw-r--r--	3658.v	3190	log plain
-rw-r--r--	3660.v	1203	log plain
-rw-r--r--	3661.v	4091	log plain
-rw-r--r--	3662.v	887	log plain
-rw-r--r--	3664.v	588	log plain
-rw-r--r--	3665.v	1174	log plain
-rw-r--r--	3666.v	1845	log plain
-rw-r--r--	3667.v	1037	log plain
-rw-r--r--	3668.v	2333	log plain
-rw-r--r--	3672.v	733	log plain
-rw-r--r--	38.v	491	log plain
-rw-r--r--	545.v	122	log plain
-rw-r--r--	808_2411.v	502	log plain
-rw-r--r--	846.v	4477	log plain
-rw-r--r--	931.v	113	log plain
-rw-r--r--	HoTT_coq_001.v	143	log plain
-rw-r--r--	HoTT_coq_002.v	915	log plain
-rw-r--r--	HoTT_coq_006.v	3846	log plain
-rw-r--r--	HoTT_coq_007.v	3977	log plain
-rw-r--r--	HoTT_coq_010.v	116	log plain
-rw-r--r--	HoTT_coq_012.v	136	log plain
-rw-r--r--	HoTT_coq_013.v	880	log plain
-rw-r--r--	HoTT_coq_014.v	7521	log plain
-rw-r--r--	HoTT_coq_016.v	590	log plain
-rw-r--r--	HoTT_coq_020.v	3311	log plain
-rw-r--r--	HoTT_coq_023.v	503	log plain
-rw-r--r--	HoTT_coq_025.v	830	log plain
-rw-r--r--	HoTT_coq_027.v	3958	log plain
-rw-r--r--	HoTT_coq_028.v	552	log plain
-rw-r--r--	HoTT_coq_029.v	12077	log plain
-rw-r--r--	HoTT_coq_030.v	9103	log plain
-rw-r--r--	HoTT_coq_032.v	656	log plain
-rw-r--r--	HoTT_coq_034.v	659	log plain
-rw-r--r--	HoTT_coq_035.v	633	log plain
-rw-r--r--	HoTT_coq_036.v	4293	log plain
-rw-r--r--	HoTT_coq_037.v	434	log plain
-rw-r--r--	HoTT_coq_041.v	706	log plain
-rw-r--r--	HoTT_coq_042.v	736	log plain
-rw-r--r--	HoTT_coq_043.v	619	log plain
-rw-r--r--	HoTT_coq_044.v	1130	log plain
-rw-r--r--	HoTT_coq_045.v	1547	log plain
-rw-r--r--	HoTT_coq_047.v	991	log plain
-rw-r--r--	HoTT_coq_048.v	232	log plain
-rw-r--r--	HoTT_coq_049.v	247	log plain
-rw-r--r--	HoTT_coq_050.v	894	log plain
-rw-r--r--	HoTT_coq_052.v	433	log plain
-rw-r--r--	HoTT_coq_053.v	1200	log plain
-rw-r--r--	HoTT_coq_054.v	3201	log plain
-rw-r--r--	HoTT_coq_055.v	2463	log plain
-rw-r--r--	HoTT_coq_056.v	5951	log plain
-rw-r--r--	HoTT_coq_057.v	766	log plain
-rw-r--r--	HoTT_coq_058.v	5885	log plain
-rw-r--r--	HoTT_coq_059.v	672	log plain
-rw-r--r--	HoTT_coq_061.v	4604	log plain
-rw-r--r--	HoTT_coq_062.v	3807	log plain
-rw-r--r--	HoTT_coq_063.v	839	log plain
-rw-r--r--	HoTT_coq_064.v	5740	log plain
-rw-r--r--	HoTT_coq_067.v	1154	log plain
-rw-r--r--	HoTT_coq_068.v	1339	log plain
-rw-r--r--	HoTT_coq_071.v	165	log plain
-rw-r--r--	HoTT_coq_074.v	214	log plain
-rw-r--r--	HoTT_coq_077.v	1098	log plain
-rw-r--r--	HoTT_coq_078.v	1360	log plain
-rw-r--r--	HoTT_coq_079.v	404	log plain
-rw-r--r--	HoTT_coq_080.v	676	log plain
-rw-r--r--	HoTT_coq_081.v	421	log plain
-rw-r--r--	HoTT_coq_082.v	475	log plain
-rw-r--r--	HoTT_coq_083.v	584	log plain
-rw-r--r--	HoTT_coq_084.v	963	log plain
-rw-r--r--	HoTT_coq_085.v	2536	log plain
-rw-r--r--	HoTT_coq_087.v	372	log plain
-rw-r--r--	HoTT_coq_088.v	3119	log plain
-rw-r--r--	HoTT_coq_089.v	1296	log plain
-rw-r--r--	HoTT_coq_090.v	6542	log plain
-rw-r--r--	HoTT_coq_091.v	6405	log plain
-rw-r--r--	HoTT_coq_093.v	758	log plain
-rw-r--r--	HoTT_coq_094.v	445	log plain
-rw-r--r--	HoTT_coq_097.v	213	log plain
-rw-r--r--	HoTT_coq_098.v	2140	log plain
-rw-r--r--	HoTT_coq_099.v	2585	log plain
-rw-r--r--	HoTT_coq_100.v	5427	log plain
-rw-r--r--	HoTT_coq_101.v	2398	log plain
-rw-r--r--	HoTT_coq_102.v	1000	log plain
-rw-r--r--	HoTT_coq_103.v	146	log plain
-rw-r--r--	HoTT_coq_104.v	317	log plain
-rw-r--r--	HoTT_coq_105.v	855	log plain
-rw-r--r--	HoTT_coq_107.v	3388	log plain
-rw-r--r--	HoTT_coq_108.v	4606	log plain
-rw-r--r--	HoTT_coq_110.v	752	log plain
-rw-r--r--	HoTT_coq_111.v	675	log plain
-rw-r--r--	HoTT_coq_112.v	2722	log plain
-rw-r--r--	HoTT_coq_113.v	727	log plain
-rw-r--r--	HoTT_coq_114.v	60	log plain
-rw-r--r--	HoTT_coq_115.v	83	log plain
-rw-r--r--	HoTT_coq_116.v	316	log plain
-rw-r--r--	HoTT_coq_117.v	903	log plain
-rw-r--r--	HoTT_coq_118.v	1443	log plain
-rw-r--r--	HoTT_coq_121.v	884	log plain
-rw-r--r--	HoTT_coq_122.v	838	log plain
-rw-r--r--	HoTT_coq_123.v	5689	log plain
-rw-r--r--	HoTT_coq_124.v	1502	log plain