aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
ModeNameSize
-rw-r--r--1100.v197logplain
-rw-r--r--121.v420logplain
-rw-r--r--1243.v195logplain
-rw-r--r--1302.v259logplain
-rw-r--r--1322.v567logplain
-rw-r--r--1411.v922logplain
-rw-r--r--1414.v1186logplain
-rw-r--r--1416.v962logplain
-rw-r--r--1419.v110logplain
-rw-r--r--1425.v481logplain
-rw-r--r--1446.v350logplain
-rw-r--r--1448.v638logplain
-rw-r--r--1477.v312logplain
-rw-r--r--1483.v150logplain
-rw-r--r--1507.v4534logplain
-rw-r--r--1519.v310logplain
-rw-r--r--1568.v185logplain
-rw-r--r--1576.v468logplain
-rw-r--r--1582.v242logplain
-rw-r--r--1604.v171logplain
-rw-r--r--1614.v487logplain
-rw-r--r--1618.v408logplain
-rw-r--r--1634.v631logplain
-rw-r--r--1643.v475logplain
-rw-r--r--1680.v190logplain
-rw-r--r--1683.v995logplain
-rw-r--r--1696.v432logplain
-rw-r--r--1703.v196logplain
-rw-r--r--1704.v421logplain
-rw-r--r--1711.v1006logplain
-rw-r--r--1718.v182logplain
-rw-r--r--1738.v622logplain
-rw-r--r--1740.v471logplain
-rw-r--r--1754.v673logplain
-rw-r--r--1773.v234logplain
-rw-r--r--1774.v512logplain
-rw-r--r--1775.v1016logplain
-rw-r--r--1776.v620logplain
-rw-r--r--1779.v836logplain
-rw-r--r--1780.v291logplain
-rw-r--r--1784.v2931logplain
-rw-r--r--1787.v264logplain
-rw-r--r--1791.v823logplain
-rw-r--r--1834.v5043logplain
-rw-r--r--1844.v7442logplain
-rw-r--r--1865.v418logplain
-rw-r--r--1891.v306logplain
-rw-r--r--1898.v129logplain
-rw-r--r--1900.v99logplain
-rw-r--r--1901.v301logplain
-rw-r--r--1905.v221logplain
-rw-r--r--1907.v169logplain
-rw-r--r--1912.v84logplain
-rw-r--r--1915.v115logplain
-rw-r--r--1918.v9247logplain
-rw-r--r--1925.v731logplain
-rw-r--r--1931.v610logplain
-rw-r--r--1935.v362logplain
-rw-r--r--1939.v356logplain
-rw-r--r--1944.v224logplain
-rw-r--r--1951.v1616logplain
-rw-r--r--1962.v1415logplain
-rw-r--r--1963.v550logplain
-rw-r--r--1977.v76logplain
-rw-r--r--1981.v103logplain
-rw-r--r--2001.v355logplain
-rw-r--r--2006.v598logplain
-rw-r--r--2016.v1914logplain
-rw-r--r--2017.v488logplain
-rw-r--r--2021.v571logplain
-rw-r--r--2027.v226logplain
-rw-r--r--2083.v683logplain
-rw-r--r--2089.v599logplain
-rw-r--r--2095.v312logplain
-rw-r--r--2105.v49logplain
-rw-r--r--2108.v407logplain
-rw-r--r--2117.v2177logplain
-rw-r--r--2123.v297logplain
-rw-r--r--2127.v238logplain
-rw-r--r--2135.v310logplain
-rw-r--r--2136.v1494logplain
-rw-r--r--2137.v1271logplain
-rw-r--r--2139.v730logplain
-rw-r--r--2141.v317logplain
-rw-r--r--2145.v414logplain
-rw-r--r--2149.v107logplain
-rw-r--r--2164.v10782logplain
-rw-r--r--2181.v74logplain
-rw-r--r--2193.v1123logplain
-rw-r--r--2230.v97logplain
-rw-r--r--2231.v134logplain
-rw-r--r--2243.v163logplain
-rw-r--r--2244.v520logplain
-rw-r--r--2250.v122logplain
-rw-r--r--2251.v195logplain
-rw-r--r--2255.v766logplain
-rw-r--r--2262.v206logplain
-rw-r--r--2281.v1204logplain
-rw-r--r--2295.v270logplain
-rw-r--r--2299.v220logplain
-rw-r--r--2300.v247logplain
-rw-r--r--2303.v139logplain
-rw-r--r--2304.v145logplain
-rw-r--r--2307.v102logplain
-rw-r--r--2310.v637logplain
-rw-r--r--2319.v299logplain
-rw-r--r--2320.v564logplain
-rw-r--r--2342.v237logplain
-rw-r--r--2347.v352logplain
-rw-r--r--2350.v187logplain
-rw-r--r--2353.v496logplain
-rw-r--r--2360.v367logplain
-rw-r--r--2362.v860logplain
-rw-r--r--2375.v354logplain
-rw-r--r--2378.v21329logplain
-rw-r--r--2388.v355logplain
-rw-r--r--2393.v286logplain
-rw-r--r--2404.v1422logplain
-rw-r--r--2406.v211logplain
-rw-r--r--2447.v207logplain
-rw-r--r--2464.v1239logplain
-rw-r--r--2467.v1551logplain
-rw-r--r--2473.v1100logplain
-rw-r--r--2584.v2261logplain
-rw-r--r--2586.v134logplain
-rw-r--r--2590.v438logplain
-rw-r--r--2602.v138logplain
-rw-r--r--2603.v891logplain
-rw-r--r--2608.v948logplain
-rw-r--r--2613.v424logplain
-rw-r--r--2615.v645logplain
-rw-r--r--2616.v203logplain
-rw-r--r--2629.v729logplain
-rw-r--r--2640.v329logplain
-rw-r--r--2667.v445logplain
-rw-r--r--2668.v169logplain
-rw-r--r--2670.v778logplain
-rw-r--r--2680.v281logplain
-rw-r--r--2713.v406logplain
-rw-r--r--2729.v4138logplain
-rw-r--r--2732.v320logplain
-rw-r--r--2733.v885logplain
-rw-r--r--2734.v344logplain
-rw-r--r--2750.v333logplain
-rw-r--r--2775.v196logplain
-rw-r--r--2810.v134logplain
-rw-r--r--2817.v291logplain
-rw-r--r--2818.v86logplain
-rw-r--r--2828.v114logplain
-rw-r--r--2830.v7794logplain
-rw-r--r--2834.v106logplain
-rw-r--r--2836.v1357logplain
-rw-r--r--2837.v403logplain
-rw-r--r--2839.v272logplain
-rw-r--r--2846.v51logplain
-rw-r--r--2848.v269logplain
-rw-r--r--2850.v49logplain
-rw-r--r--2854.v147logplain
-rw-r--r--2876.v291logplain
-rw-r--r--2883.v873logplain
-rw-r--r--2900.v813logplain
-rw-r--r--2920.v136logplain
-rw-r--r--2923.v240logplain
-rw-r--r--2928.v346logplain
-rw-r--r--2930.v292logplain
-rw-r--r--2945.v200logplain
-rw-r--r--2946.v407logplain
-rw-r--r--2951.v57logplain
-rw-r--r--2955.v664logplain
-rw-r--r--2966.v1879logplain
-rw-r--r--2969.v569logplain
-rw-r--r--2981.v702logplain
-rw-r--r--2983.v127logplain
-rw-r--r--2990.v121logplain
-rw-r--r--2994.v75logplain
-rw-r--r--2995.v241logplain
-rw-r--r--2996.v608logplain
-rw-r--r--3000.v112logplain
-rw-r--r--3001.v769logplain
-rw-r--r--3003.v524logplain
-rw-r--r--3004.v246logplain
-rw-r--r--3008.v664logplain
-rw-r--r--3010b.v143logplain
-rw-r--r--3016.v90logplain
-rw-r--r--3017.v160logplain
-rw-r--r--3022.v250logplain
-rw-r--r--3023.v843logplain
-rw-r--r--3036.v4805logplain
-rw-r--r--3037.v322logplain
-rw-r--r--3043.v148logplain
-rw-r--r--3045.v1465logplain
-rw-r--r--3050.v116logplain
-rw-r--r--3054.v81logplain
-rw-r--r--3062.v105logplain
-rw-r--r--3068.v1688logplain
-rw-r--r--3071.v74logplain
-rw-r--r--3088.v372logplain
-rw-r--r--3093.v126logplain
-rw-r--r--3142.v377logplain
-rw-r--r--3164.v1231logplain
-rw-r--r--3188.v632logplain
-rw-r--r--3199.v412logplain
-rw-r--r--3205.v807logplain
-rw-r--r--3210.v549logplain
-rw-r--r--3212.v143logplain
-rw-r--r--3217.v765logplain
-rw-r--r--3228.v169logplain
-rw-r--r--3242.v46logplain
-rw-r--r--3249.v331logplain
-rw-r--r--3251.v515logplain
-rw-r--r--3258.v1126logplain
-rw-r--r--3259.v274logplain
-rw-r--r--3260.v142logplain
-rw-r--r--3262.v2700logplain
-rw-r--r--3264.v946logplain
-rw-r--r--3265.v236logplain
-rw-r--r--3266.v74logplain
-rw-r--r--3267.v1067logplain
-rw-r--r--328.v786logplain
-rw-r--r--3281.v149logplain
-rw-r--r--3282.v257logplain
-rw-r--r--3284.v827logplain
-rw-r--r--3285.v106logplain
-rw-r--r--3286.v1595logplain
-rw-r--r--3287.v308logplain
-rw-r--r--3289.v829logplain
-rw-r--r--329.v2353logplain
-rw-r--r--3291.v348logplain
-rw-r--r--3294.v204logplain
-rw-r--r--3297.v328logplain
-rw-r--r--3298.v481logplain
-rw-r--r--3300.v214logplain
-rw-r--r--3305.v264logplain
-rw-r--r--3306.v281logplain
-rw-r--r--331.v262logplain
-rw-r--r--3310.v297logplain
-rw-r--r--3314.v4000logplain
-rw-r--r--3315.v1175logplain
-rw-r--r--3317.v3799logplain
-rw-r--r--3319.v1081logplain
-rw-r--r--3321.v1295logplain
-rw-r--r--3322.v1243logplain
-rw-r--r--3323.v4228logplain
-rw-r--r--3324.v1922logplain
-rw-r--r--3325.v1290logplain
-rw-r--r--3326.v302logplain
-rw-r--r--3329.v3943logplain
-rw-r--r--3330.v28712logplain
-rw-r--r--3331.v1557logplain
-rw-r--r--3332.v259logplain
-rw-r--r--3336.v229logplain
-rw-r--r--3337.v102logplain
-rw-r--r--3338.v111logplain
-rw-r--r--3344.v2650logplain
-rw-r--r--3346.v230logplain
-rw-r--r--3347.v2208logplain
-rw-r--r--3348.v247logplain
-rw-r--r--335.v107logplain
-rw-r--r--3350.v4270logplain
-rw-r--r--3352.v1781logplain
-rw-r--r--3354.v386logplain
-rw-r--r--3355.v167logplain
-rw-r--r--3368.v871logplain
-rw-r--r--3372.v318logplain
-rw-r--r--3373.v1380logplain
-rw-r--r--3374.v2493logplain
-rw-r--r--3375.v2832logplain
-rw-r--r--3377.v444logplain
-rw-r--r--3382.v3258logplain
-rw-r--r--3386.v556logplain
-rw-r--r--3387.v591logplain
-rw-r--r--3388.v1280logplain
-rw-r--r--3390.v353logplain
-rw-r--r--3392.v2400logplain
-rw-r--r--3393.v6737logplain
-rw-r--r--3402.v187logplain
-rw-r--r--3408.v7644logplain
-rw-r--r--3416.v390logplain
-rw-r--r--3417.v113logplain
-rw-r--r--3422.v6827logplain
-rw-r--r--3424.v954logplain
-rw-r--r--3427.v8179logplain
-rw-r--r--3428.v1401logplain
-rw-r--r--3439.v1611logplain
-rw-r--r--3446.v2706logplain
-rw-r--r--3453.v281logplain
-rw-r--r--3454.v2468logplain
-rw-r--r--3461.v90logplain
-rw-r--r--3467.v86logplain
-rw-r--r--3469.v974logplain
-rw-r--r--3477.v294logplain
-rw-r--r--348.v186logplain
-rw-r--r--3480.v2185logplain
-rw-r--r--3481.v1823logplain
-rw-r--r--3482.v394logplain
-rw-r--r--3483.v164logplain
-rw-r--r--3484.v1264logplain
-rw-r--r--3485.v5321logplain
-rw-r--r--3487.v255logplain
-rw-r--r--3490.v1521logplain
-rw-r--r--3491.v254logplain
-rw-r--r--3505.v1976logplain
-rw-r--r--3509.v222logplain
-rw-r--r--3510.v202logplain
-rw-r--r--3513.v3987logplain
-rw-r--r--3520.v200logplain
-rw-r--r--3531.v2402logplain
-rw-r--r--3537.v314logplain
-rw-r--r--3539.v3344logplain
-rw-r--r--3542.v236logplain
-rw-r--r--3546.v485logplain
-rw-r--r--3559.v3527logplain
-rw-r--r--3560.v748logplain
-rw-r--r--3561.v1274logplain
-rw-r--r--3562.v197logplain
-rw-r--r--3563.v1802logplain
-rw-r--r--3566.v1164logplain
-rw-r--r--3567.v3272logplain
-rw-r--r--3584.v720logplain
-rw-r--r--3590.v379logplain
-rw-r--r--3593.v359logplain
-rw-r--r--3594.v2653logplain
-rw-r--r--3596.v513logplain
-rw-r--r--3612.v2766logplain
-rw-r--r--3616.v154logplain
-rw-r--r--3618.v3790logplain
-rw-r--r--3623.v138logplain
-rw-r--r--3624.v285logplain
-rw-r--r--3625.v260logplain
-rw-r--r--3628.v191logplain
-rw-r--r--3633.v330logplain
-rw-r--r--3637.v327logplain
-rw-r--r--3638.v1360logplain
-rw-r--r--3640.v1441logplain
-rw-r--r--3641.v1236logplain
-rw-r--r--3647.v23042logplain
-rw-r--r--3648.v3129logplain
-rw-r--r--3649.v3043logplain
-rw-r--r--3652.v2778logplain
-rw-r--r--3653.v251logplain
-rw-r--r--3654.v172logplain
-rw-r--r--3656.v1464logplain
-rw-r--r--3657.v430logplain
-rw-r--r--3658.v3222logplain
-rw-r--r--3660.v1235logplain
-rw-r--r--3661.v4091logplain
-rw-r--r--3662.v887logplain
-rw-r--r--3664.v620logplain
-rw-r--r--3665.v1174logplain
-rw-r--r--3666.v1880logplain
-rw-r--r--3667.v1037logplain
-rw-r--r--3668.v2385logplain
-rw-r--r--3670.v372logplain
-rw-r--r--3672.v733logplain
-rw-r--r--3675.v1161logplain
-rw-r--r--3681.v432logplain
-rw-r--r--3682.v160logplain
-rw-r--r--3684.v97logplain
-rw-r--r--3685.v3034logplain
-rw-r--r--3686.v2535logplain
-rw-r--r--3690.v1410logplain
-rw-r--r--3692.v1454logplain
-rw-r--r--3698.v1571logplain
-rw-r--r--3699.v7504logplain
-rw-r--r--3700.v3177logplain
-rw-r--r--3703.v1334logplain
-rw-r--r--3709.v664logplain
-rw-r--r--3710.v2684logplain
-rw-r--r--3723.v187logplain
-rw-r--r--3732.v4096logplain
-rw-r--r--3736.v234logplain
-rw-r--r--3743.v567logplain
-rw-r--r--3755.v731logplain
-rw-r--r--3777.v624logplain
-rw-r--r--3779.v645logplain
-rw-r--r--3782.v2646logplain
-rw-r--r--3783.v909logplain
-rw-r--r--3786.v1309logplain
-rw-r--r--3788.v359logplain
-rw-r--r--3792.v154logplain
-rw-r--r--3798.v234logplain
-rw-r--r--38.v491logplain
-rw-r--r--3804.v223logplain
-rw-r--r--3808.v131logplain
-rw-r--r--3815.v300logplain
-rw-r--r--3819.v224logplain
-rw-r--r--3821.v109logplain
-rw-r--r--3828.v29logplain
-rw-r--r--3854.v982logplain
-rw-r--r--3881.v2318logplain
-rw-r--r--3892.v443logplain
-rw-r--r--3895.v942logplain
-rw-r--r--3896.v92logplain
-rw-r--r--3899.v367logplain
-rw-r--r--3900.v534logplain
-rw-r--r--3916.v51logplain
-rw-r--r--3922.v2695logplain
-rw-r--r--3938.v286logplain
-rw-r--r--3944.v130logplain
-rw-r--r--3948.v389logplain
-rw-r--r--3953.v152logplain
-rw-r--r--3956.v4704logplain
-rw-r--r--3960.v371logplain
-rw-r--r--3974.v189logplain
-rw-r--r--3975.v187logplain
-rw-r--r--3978.v543logplain
-rw-r--r--3993.v115logplain
-rw-r--r--4001.v469logplain
-rw-r--r--4012.v89logplain
-rw-r--r--4016.v230logplain
-rw-r--r--4017.v262logplain
-rw-r--r--4018.v96logplain
-rw-r--r--4031.v370logplain
-rw-r--r--4034.v707logplain
-rw-r--r--4035.v578logplain
-rw-r--r--4046.v159logplain
-rw-r--r--4057.v7311logplain
-rw-r--r--4069.v1126logplain
-rw-r--r--4078.v140logplain
-rw-r--r--4089.v11760logplain
-rw-r--r--4097.v3129logplain
-rw-r--r--4101.v927logplain
-rw-r--r--4103.v313logplain
-rw-r--r--4116.v12195logplain
-rw-r--r--4120.v210logplain
-rw-r--r--4121.v1020logplain
-rw-r--r--4151.v17541logplain
-rw-r--r--4161.v704logplain
-rw-r--r--4165.v177logplain
-rw-r--r--4190.v215logplain
-rw-r--r--4191.v230logplain
-rw-r--r--4193.v89logplain
-rw-r--r--4198.v1015logplain
-rw-r--r--4203.v619logplain
-rw-r--r--4205.v262logplain
-rw-r--r--4216.v699logplain
-rw-r--r--4217.v163logplain
-rw-r--r--4221.v297logplain
-rw-r--r--4232.v594logplain
-rw-r--r--4234.v200logplain
-rw-r--r--4240.v249logplain
-rw-r--r--4251.v442logplain
-rw-r--r--4254.v302logplain
-rw-r--r--4272.v250logplain
-rw-r--r--4276.v301logplain
-rw-r--r--4280.v669logplain
-rw-r--r--4283.v280logplain
-rw-r--r--4287.v2918logplain
-rw-r--r--4294.v668logplain
-rw-r--r--4298.v126logplain
-rw-r--r--4299.v288logplain
-rw-r--r--4301.v239logplain
-rw-r--r--4305.v265logplain
-rw-r--r--4316.v49logplain
-rw-r--r--4318.v91logplain
-rw-r--r--4325.v105logplain
-rw-r--r--4328.v357logplain
-rw-r--r--4346.v43logplain
-rw-r--r--4347.v589logplain
-rw-r--r--4354.v338logplain
-rw-r--r--4366.v209logplain
-rw-r--r--4372.v476logplain
-rw-r--r--4375.v1920logplain
-rw-r--r--4390.v623logplain
-rw-r--r--4394.v793logplain
-rw-r--r--4397.v93logplain
-rw-r--r--545.v122logplain
-rw-r--r--808_2411.v502logplain
-rw-r--r--846.v4477logplain
-rw-r--r--931.v113logplain
-rw-r--r--HoTT_coq_001.v143logplain
-rw-r--r--HoTT_coq_002.v915logplain
-rw-r--r--HoTT_coq_006.v3846logplain
-rw-r--r--HoTT_coq_007.v4044logplain
-rw-r--r--HoTT_coq_010.v116logplain
-rw-r--r--HoTT_coq_012.v136logplain
-rw-r--r--HoTT_coq_013.v880logplain
-rw-r--r--HoTT_coq_014.v7656logplain
-rw-r--r--HoTT_coq_016.v590logplain
-rw-r--r--HoTT_coq_020.v3343logplain
-rw-r--r--HoTT_coq_023.v503logplain
-rw-r--r--HoTT_coq_025.v830logplain
-rw-r--r--HoTT_coq_027.v3958logplain
-rw-r--r--HoTT_coq_028.v552logplain
-rw-r--r--HoTT_coq_029.v12109logplain
-rw-r--r--HoTT_coq_030.v9135logplain
-rw-r--r--HoTT_coq_032.v656logplain
-rw-r--r--HoTT_coq_034.v659logplain
-rw-r--r--HoTT_coq_035.v665logplain
-rw-r--r--HoTT_coq_036.v4328logplain
-rw-r--r--HoTT_coq_037.v434logplain
-rw-r--r--HoTT_coq_041.v706logplain
-rw-r--r--HoTT_coq_042.v768logplain
-rw-r--r--HoTT_coq_043.v619logplain
-rw-r--r--HoTT_coq_044.v1130logplain
-rw-r--r--HoTT_coq_045.v1547logplain
-rw-r--r--HoTT_coq_047.v991logplain
-rw-r--r--HoTT_coq_048.v232logplain
-rw-r--r--HoTT_coq_049.v247logplain
-rw-r--r--HoTT_coq_050.v894logplain
-rw-r--r--HoTT_coq_052.v433logplain
-rw-r--r--HoTT_coq_053.v1199logplain
-rw-r--r--HoTT_coq_054.v3201logplain
-rw-r--r--HoTT_coq_055.v2495logplain
-rw-r--r--HoTT_coq_056.v5983logplain
-rw-r--r--HoTT_coq_057.v766logplain
-rw-r--r--HoTT_coq_058.v5917logplain
-rw-r--r--HoTT_coq_059.v672logplain
-rw-r--r--HoTT_coq_061.v4636logplain
-rw-r--r--HoTT_coq_062.v3874logplain
-rw-r--r--HoTT_coq_063.v839logplain
-rw-r--r--HoTT_coq_064.v5772logplain
-rw-r--r--HoTT_coq_067.v1186logplain
-rw-r--r--HoTT_coq_068.v1339logplain
-rw-r--r--HoTT_coq_071.v165logplain
-rw-r--r--HoTT_coq_074.v214logplain
-rw-r--r--HoTT_coq_077.v1098logplain
-rw-r--r--HoTT_coq_078.v1360logplain
-rw-r--r--HoTT_coq_079.v404logplain
-rw-r--r--HoTT_coq_080.v676logplain
-rw-r--r--HoTT_coq_081.v421logplain
-rw-r--r--HoTT_coq_082.v475logplain
-rw-r--r--HoTT_coq_083.v584logplain
-rw-r--r--HoTT_coq_084.v963logplain
-rw-r--r--HoTT_coq_085.v2536logplain
-rw-r--r--HoTT_coq_087.v372logplain
-rw-r--r--HoTT_coq_088.v3151logplain
-rw-r--r--HoTT_coq_089.v1296logplain
-rw-r--r--HoTT_coq_090.v6574logplain
-rw-r--r--HoTT_coq_091.v6405logplain
-rw-r--r--HoTT_coq_093.v797logplain
-rw-r--r--HoTT_coq_094.v445logplain
-rw-r--r--HoTT_coq_097.v213logplain
-rw-r--r--HoTT_coq_098.v2172logplain
-rw-r--r--HoTT_coq_099.v2617logplain
-rw-r--r--HoTT_coq_100.v5459logplain
-rw-r--r--HoTT_coq_101.v2430logplain
-rw-r--r--HoTT_coq_102.v1032logplain
-rw-r--r--HoTT_coq_103.v146logplain
-rw-r--r--HoTT_coq_104.v317logplain
-rw-r--r--HoTT_coq_105.v855logplain
-rw-r--r--HoTT_coq_107.v3425logplain
-rw-r--r--HoTT_coq_108.v4638logplain
-rw-r--r--HoTT_coq_110.v752logplain
-rw-r--r--HoTT_coq_111.v675logplain
-rw-r--r--HoTT_coq_112.v2754logplain
-rw-r--r--HoTT_coq_113.v759logplain
-rw-r--r--HoTT_coq_114.v60logplain
-rw-r--r--HoTT_coq_115.v83logplain
-rw-r--r--HoTT_coq_116.v316logplain
-rw-r--r--HoTT_coq_117.v903logplain
-rw-r--r--HoTT_coq_118.v1475logplain
-rw-r--r--HoTT_coq_120.v5432logplain
-rw-r--r--HoTT_coq_121.v916logplain
-rw-r--r--HoTT_coq_122.v838logplain
-rw-r--r--HoTT_coq_123.v5721logplain
-rw-r--r--HoTT_coq_124.v1502logplain