closed « bugs « test-suite - debian-coq

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	421	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--	2016.v	1914	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--	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--	2149.v	107	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--	2243.v	163	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	21329	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	211	log plain
-rw-r--r--	2447.v	207	log plain
-rw-r--r--	2464.v	1239	log plain
-rw-r--r--	2467.v	1551	log plain
-rw-r--r--	2473.v	1100	log plain
-rw-r--r--	2584.v	2261	log plain
-rw-r--r--	2586.v	134	log plain
-rw-r--r--	2590.v	438	log plain
-rw-r--r--	2602.v	138	log plain
-rw-r--r--	2603.v	891	log plain
-rw-r--r--	2608.v	948	log plain
-rw-r--r--	2613.v	424	log plain
-rw-r--r--	2615.v	645	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--	2713.v	406	log plain
-rw-r--r--	2729.v	4138	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--	2775.v	196	log plain
-rw-r--r--	2810.v	134	log plain
-rw-r--r--	2817.v	291	log plain
-rw-r--r--	2818.v	86	log plain
-rw-r--r--	2828.v	114	log plain
-rw-r--r--	2830.v	7794	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--	2850.v	49	log plain
-rw-r--r--	2854.v	147	log plain
-rw-r--r--	2876.v	291	log plain
-rw-r--r--	2883.v	873	log plain
-rw-r--r--	2900.v	813	log plain
-rw-r--r--	2920.v	136	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--	2945.v	200	log plain
-rw-r--r--	2946.v	407	log plain
-rw-r--r--	2951.v	57	log plain
-rw-r--r--	2955.v	664	log plain
-rw-r--r--	2966.v	1879	log plain
-rw-r--r--	2969.v	569	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	608	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--	3045.v	1465	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--	3068.v	1688	log plain
-rw-r--r--	3071.v	74	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--	3199.v	412	log plain
-rw-r--r--	3205.v	807	log plain
-rw-r--r--	3210.v	549	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--	3249.v	331	log plain
-rw-r--r--	3251.v	515	log plain
-rw-r--r--	3258.v	1126	log plain
-rw-r--r--	3259.v	274	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	1067	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--	3298.v	481	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--	331.v	262	log plain
-rw-r--r--	3310.v	297	log plain
-rw-r--r--	3314.v	4000	log plain
-rw-r--r--	3315.v	1175	log plain
-rw-r--r--	3317.v	3799	log plain
-rw-r--r--	3319.v	1081	log plain
-rw-r--r--	3321.v	1295	log plain
-rw-r--r--	3322.v	1243	log plain
-rw-r--r--	3323.v	4228	log plain
-rw-r--r--	3324.v	1922	log plain
-rw-r--r--	3325.v	1290	log plain
-rw-r--r--	3326.v	302	log plain
-rw-r--r--	3329.v	3943	log plain
-rw-r--r--	3330.v	28712	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	2650	log plain
-rw-r--r--	3346.v	230	log plain
-rw-r--r--	3347.v	2208	log plain
-rw-r--r--	3348.v	247	log plain
-rw-r--r--	335.v	107	log plain
-rw-r--r--	3350.v	4270	log plain
-rw-r--r--	3352.v	1781	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	1380	log plain
-rw-r--r--	3374.v	2493	log plain
-rw-r--r--	3375.v	2832	log plain
-rw-r--r--	3377.v	444	log plain
-rw-r--r--	3382.v	3258	log plain
-rw-r--r--	3386.v	556	log plain
-rw-r--r--	3387.v	591	log plain
-rw-r--r--	3388.v	1280	log plain
-rw-r--r--	3390.v	353	log plain
-rw-r--r--	3392.v	2400	log plain
-rw-r--r--	3393.v	6737	log plain
-rw-r--r--	3402.v	187	log plain
-rw-r--r--	3408.v	7644	log plain
-rw-r--r--	3416.v	390	log plain
-rw-r--r--	3417.v	113	log plain
-rw-r--r--	3422.v	6827	log plain
-rw-r--r--	3424.v	954	log plain
-rw-r--r--	3427.v	8179	log plain
-rw-r--r--	3428.v	1401	log plain
-rw-r--r--	3439.v	1611	log plain
-rw-r--r--	3446.v	2706	log plain
-rw-r--r--	3453.v	281	log plain
-rw-r--r--	3454.v	2468	log plain
-rw-r--r--	3461.v	90	log plain
-rw-r--r--	3467.v	86	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	2185	log plain
-rw-r--r--	3481.v	1823	log plain
-rw-r--r--	3482.v	394	log plain
-rw-r--r--	3483.v	164	log plain
-rw-r--r--	3484.v	1264	log plain
-rw-r--r--	3485.v	5321	log plain
-rw-r--r--	3487.v	255	log plain
-rw-r--r--	3490.v	1521	log plain
-rw-r--r--	3491.v	254	log plain
-rw-r--r--	3505.v	1976	log plain
-rw-r--r--	3509.v	222	log plain
-rw-r--r--	3510.v	202	log plain
-rw-r--r--	3513.v	3987	log plain
-rw-r--r--	3520.v	200	log plain
-rw-r--r--	3531.v	2402	log plain
-rw-r--r--	3537.v	314	log plain
-rw-r--r--	3539.v	3344	log plain
-rw-r--r--	3542.v	236	log plain
-rw-r--r--	3546.v	485	log plain
-rw-r--r--	3559.v	3527	log plain
-rw-r--r--	3560.v	748	log plain
-rw-r--r--	3561.v	1274	log plain
-rw-r--r--	3562.v	197	log plain
-rw-r--r--	3563.v	1802	log plain
-rw-r--r--	3566.v	1164	log plain
-rw-r--r--	3567.v	3272	log plain
-rw-r--r--	3584.v	720	log plain
-rw-r--r--	3590.v	379	log plain
-rw-r--r--	3593.v	359	log plain
-rw-r--r--	3594.v	2653	log plain
-rw-r--r--	3596.v	513	log plain
-rw-r--r--	3612.v	2766	log plain
-rw-r--r--	3616.v	154	log plain
-rw-r--r--	3618.v	3790	log plain
-rw-r--r--	3623.v	138	log plain
-rw-r--r--	3624.v	285	log plain
-rw-r--r--	3625.v	260	log plain
-rw-r--r--	3628.v	191	log plain
-rw-r--r--	3633.v	330	log plain
-rw-r--r--	3637.v	327	log plain
-rw-r--r--	3638.v	1360	log plain
-rw-r--r--	3640.v	1441	log plain
-rw-r--r--	3641.v	1236	log plain
-rw-r--r--	3647.v	23042	log plain
-rw-r--r--	3648.v	3129	log plain
-rw-r--r--	3649.v	3043	log plain
-rw-r--r--	3652.v	2778	log plain
-rw-r--r--	3653.v	251	log plain
-rw-r--r--	3654.v	172	log plain
-rw-r--r--	3656.v	1464	log plain
-rw-r--r--	3657.v	430	log plain
-rw-r--r--	3658.v	3222	log plain
-rw-r--r--	3660.v	1235	log plain
-rw-r--r--	3661.v	4091	log plain
-rw-r--r--	3662.v	887	log plain
-rw-r--r--	3664.v	620	log plain
-rw-r--r--	3665.v	1174	log plain
-rw-r--r--	3666.v	1880	log plain
-rw-r--r--	3667.v	1037	log plain
-rw-r--r--	3668.v	2385	log plain
-rw-r--r--	3670.v	372	log plain
-rw-r--r--	3672.v	733	log plain
-rw-r--r--	3675.v	1161	log plain
-rw-r--r--	3681.v	432	log plain
-rw-r--r--	3682.v	160	log plain
-rw-r--r--	3684.v	97	log plain
-rw-r--r--	3685.v	3034	log plain
-rw-r--r--	3686.v	2535	log plain
-rw-r--r--	3690.v	1410	log plain
-rw-r--r--	3692.v	1454	log plain
-rw-r--r--	3698.v	1571	log plain
-rw-r--r--	3699.v	7504	log plain
-rw-r--r--	3700.v	3177	log plain
-rw-r--r--	3703.v	1334	log plain
-rw-r--r--	3709.v	664	log plain
-rw-r--r--	3710.v	2684	log plain
-rw-r--r--	3723.v	187	log plain
-rw-r--r--	3732.v	4096	log plain
-rw-r--r--	3736.v	234	log plain
-rw-r--r--	3743.v	567	log plain
-rw-r--r--	3755.v	731	log plain
-rw-r--r--	3777.v	624	log plain
-rw-r--r--	3779.v	645	log plain
-rw-r--r--	3782.v	2646	log plain
-rw-r--r--	3783.v	909	log plain
-rw-r--r--	3786.v	1309	log plain
-rw-r--r--	3788.v	359	log plain
-rw-r--r--	3792.v	154	log plain
-rw-r--r--	3798.v	234	log plain
-rw-r--r--	38.v	491	log plain
-rw-r--r--	3804.v	223	log plain
-rw-r--r--	3808.v	131	log plain
-rw-r--r--	3815.v	300	log plain
-rw-r--r--	3819.v	224	log plain
-rw-r--r--	3821.v	109	log plain
-rw-r--r--	3828.v	29	log plain
-rw-r--r--	3854.v	982	log plain
-rw-r--r--	3881.v	2318	log plain
-rw-r--r--	3892.v	443	log plain
-rw-r--r--	3895.v	942	log plain
-rw-r--r--	3896.v	92	log plain
-rw-r--r--	3899.v	367	log plain
-rw-r--r--	3900.v	534	log plain
-rw-r--r--	3916.v	51	log plain
-rw-r--r--	3922.v	2695	log plain
-rw-r--r--	3938.v	286	log plain
-rw-r--r--	3944.v	130	log plain
-rw-r--r--	3948.v	389	log plain
-rw-r--r--	3953.v	152	log plain
-rw-r--r--	3956.v	4704	log plain
-rw-r--r--	3960.v	371	log plain
-rw-r--r--	3974.v	189	log plain
-rw-r--r--	3975.v	187	log plain
-rw-r--r--	3978.v	543	log plain
-rw-r--r--	3993.v	115	log plain
-rw-r--r--	4001.v	469	log plain
-rw-r--r--	4012.v	89	log plain
-rw-r--r--	4016.v	230	log plain
-rw-r--r--	4017.v	262	log plain
-rw-r--r--	4018.v	96	log plain
-rw-r--r--	4031.v	370	log plain
-rw-r--r--	4034.v	707	log plain
-rw-r--r--	4035.v	578	log plain
-rw-r--r--	4046.v	159	log plain
-rw-r--r--	4057.v	7311	log plain
-rw-r--r--	4069.v	1126	log plain
-rw-r--r--	4078.v	140	log plain
-rw-r--r--	4089.v	11760	log plain
-rw-r--r--	4097.v	3129	log plain
-rw-r--r--	4101.v	927	log plain
-rw-r--r--	4103.v	313	log plain
-rw-r--r--	4116.v	12195	log plain
-rw-r--r--	4120.v	210	log plain
-rw-r--r--	4121.v	1020	log plain
-rw-r--r--	4151.v	17541	log plain
-rw-r--r--	4161.v	704	log plain
-rw-r--r--	4165.v	177	log plain
-rw-r--r--	4190.v	215	log plain
-rw-r--r--	4191.v	230	log plain
-rw-r--r--	4193.v	89	log plain
-rw-r--r--	4198.v	1015	log plain
-rw-r--r--	4203.v	619	log plain
-rw-r--r--	4205.v	262	log plain
-rw-r--r--	4216.v	699	log plain
-rw-r--r--	4217.v	163	log plain
-rw-r--r--	4221.v	297	log plain
-rw-r--r--	4232.v	594	log plain
-rw-r--r--	4234.v	200	log plain
-rw-r--r--	4240.v	249	log plain
-rw-r--r--	4251.v	442	log plain
-rw-r--r--	4254.v	302	log plain
-rw-r--r--	4272.v	250	log plain
-rw-r--r--	4276.v	301	log plain
-rw-r--r--	4280.v	669	log plain
-rw-r--r--	4283.v	280	log plain
-rw-r--r--	4287.v	2918	log plain
-rw-r--r--	4294.v	668	log plain
-rw-r--r--	4298.v	126	log plain
-rw-r--r--	4299.v	288	log plain
-rw-r--r--	4301.v	239	log plain
-rw-r--r--	4305.v	265	log plain
-rw-r--r--	4316.v	49	log plain
-rw-r--r--	4318.v	91	log plain
-rw-r--r--	4325.v	105	log plain
-rw-r--r--	4328.v	357	log plain
-rw-r--r--	4346.v	43	log plain
-rw-r--r--	4347.v	589	log plain
-rw-r--r--	4354.v	338	log plain
-rw-r--r--	4366.v	209	log plain
-rw-r--r--	4372.v	476	log plain
-rw-r--r--	4375.v	1920	log plain
-rw-r--r--	4390.v	623	log plain
-rw-r--r--	4394.v	793	log plain
-rw-r--r--	4397.v	93	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	4044	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	7677	log plain
-rw-r--r--	HoTT_coq_016.v	590	log plain
-rw-r--r--	HoTT_coq_020.v	3343	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	12109	log plain
-rw-r--r--	HoTT_coq_030.v	9135	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	665	log plain
-rw-r--r--	HoTT_coq_036.v	4328	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	768	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	1199	log plain
-rw-r--r--	HoTT_coq_054.v	3201	log plain
-rw-r--r--	HoTT_coq_055.v	2495	log plain
-rw-r--r--	HoTT_coq_056.v	5983	log plain
-rw-r--r--	HoTT_coq_057.v	766	log plain
-rw-r--r--	HoTT_coq_058.v	5917	log plain
-rw-r--r--	HoTT_coq_059.v	672	log plain
-rw-r--r--	HoTT_coq_061.v	4636	log plain
-rw-r--r--	HoTT_coq_062.v	3874	log plain
-rw-r--r--	HoTT_coq_063.v	839	log plain
-rw-r--r--	HoTT_coq_064.v	5772	log plain
-rw-r--r--	HoTT_coq_067.v	1186	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	3151	log plain
-rw-r--r--	HoTT_coq_089.v	1296	log plain
-rw-r--r--	HoTT_coq_090.v	6574	log plain
-rw-r--r--	HoTT_coq_091.v	6405	log plain
-rw-r--r--	HoTT_coq_093.v	797	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	2172	log plain
-rw-r--r--	HoTT_coq_099.v	2617	log plain
-rw-r--r--	HoTT_coq_100.v	5459	log plain
-rw-r--r--	HoTT_coq_101.v	2430	log plain
-rw-r--r--	HoTT_coq_102.v	1032	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	3425	log plain
-rw-r--r--	HoTT_coq_108.v	4638	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	2754	log plain
-rw-r--r--	HoTT_coq_113.v	759	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	1475	log plain
-rw-r--r--	HoTT_coq_120.v	5432	log plain
-rw-r--r--	HoTT_coq_121.v	916	log plain
-rw-r--r--	HoTT_coq_122.v	838	log plain
-rw-r--r--	HoTT_coq_123.v	5721	log plain
-rw-r--r--	HoTT_coq_124.v	1502	log plain