Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fixes #441
<details><summary>Timing Diff</summary>
<p>
```
After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem)
-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
55m51.35s | 3100356 ko | Total Time / Peak Mem | 54m30.12s | 3101084 ko || +1m21.23s || -728 ko | +2.48% | -0.02%
-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
1m16.14s | 1632284 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo | 1m09.01s | 1641988 ko || +0m07.12s || -9704 ko | +10.33% | -0.59%
1m13.23s | 1802048 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo | 1m05.28s | 1790720 ko || +0m07.95s || 11328 ko | +12.17% | +0.63%
0m28.45s | 1305696 ko | ToTemplate/Common/EnvironmentTyping.vo | 0m20.61s | 1301284 ko || +0m07.83s || 4412 ko | +38.03% | +0.33%
0m21.90s | 1159880 ko | ToTemplate/Template/Typing.vo | 0m17.21s | 1146964 ko || +0m04.68s || 12916 ko | +27.25% | +1.12%
0m23.80s | 1434644 ko | uGraph.vo | 0m20.31s | 1437728 ko || +0m03.49s || -3084 ko | +17.18% | -0.21%
0m16.48s | 934048 ko | ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo | 0m12.89s | 927988 ko || +0m03.58s || 6060 ko | +27.85% | +0.65%
2m14.92s | 2283076 ko | PCUICTypeChecker.vo | 2m17.63s | 2283164 ko || -0m02.71s || -88 ko | -1.96% | -0.00%
1m11.82s | 1356176 ko | PCUICParallelReductionConfluence.vo | 1m09.27s | 1351576 ko || +0m02.54s || 4600 ko | +3.68% | +0.34%
0m45.45s | 1277812 ko | ByteCompareSpec.vo | 0m42.86s | 1279880 ko || +0m02.59s || -2068 ko | +6.04% | -0.16%
0m15.47s | 1074800 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo | 0m13.38s | 1033856 ko || +0m02.08s || 40944 ko | +15.62% | +3.96%
0m12.77s | 874736 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo | 0m10.67s | 876020 ko || +0m02.09s || -1284 ko | +19.68% | -0.14%
0m07.43s | 1058920 ko | ToTemplate/Template/WfAst.vo | 0m05.36s | 1059712 ko || +0m02.06s || -792 ko | +38.61% | -0.07%
4m22.24s | 2085704 ko | PCUICSafeConversion.vo | 4m23.65s | 2085152 ko || -0m01.40s || 552 ko | -0.53% | +0.02%
0m50.56s | 2185660 ko | PCUICConversion.vo | 0m49.16s | 2181016 ko || +0m01.40s || 4644 ko | +2.84% | +0.21%
0m46.08s | 1361592 ko | Typed/OptimizeCorrectness.vo | 0m44.76s | 1361288 ko || +0m01.32s || 304 ko | +2.94% | +0.02%
0m15.28s | 870392 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo | 0m14.03s | 865688 ko || +0m01.25s || 4704 ko | +8.90% | +0.54%
0m14.89s | 859872 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo | 0m13.05s | 859148 ko || +0m01.83s || 724 ko | +14.09% | +0.08%
0m14.39s | 849784 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo | 0m12.48s | 855744 ko || +0m01.91s || -5960 ko | +15.30% | -0.69%
0m14.36s | 857096 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo | 0m12.56s | 857636 ko || +0m01.79s || -540 ko | +14.33% | -0.06%
0m12.65s | 914672 ko | Conversion/PCUICRenameConv.vo | 0m11.52s | 914804 ko || +0m01.13s || -132 ko | +9.80% | -0.01%
0m12.30s | 887812 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo | 0m11.26s | 881520 ko || +0m01.04s || 6292 ko | +9.23% | +0.71%
0m11.44s | 872644 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo | 0m09.99s | 874160 ko || +0m01.44s || -1516 ko | +14.51% | -0.17%
0m11.43s | 945104 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo | 0m09.83s | 982336 ko || +0m01.59s || -37232 ko | +16.27% | -3.79%
0m07.38s | 1059380 ko | ToTemplate/Template/TermEquality.vo | 0m05.73s | 1057968 ko || +0m01.64s || 1412 ko | +28.79% | +0.13%
0m06.49s | 986272 ko | ToTemplate/Common/Environment.vo | 0m04.73s | 985104 ko || +0m01.75s || 1168 ko | +37.20% | +0.11%
0m06.29s | 832232 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo | 0m05.27s | 828496 ko || +0m01.02s || 3736 ko | +19.35% | +0.45%
0m03.62s | 799328 ko | ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo | 0m02.53s | 801168 ko || +0m01.09s || -1840 ko | +43.08% | -0.22%
2m48.38s | 1394740 ko | PCUICRetypingEnvIrrelevance.vo | 2m48.94s | 1392792 ko || -0m00.56s || 1948 ko | -0.33% | +0.13%
2m39.53s | 3100356 ko | ErasureFunction.vo | 2m39.98s | 3101084 ko || -0m00.44s || -728 ko | -0.28% | -0.02%
1m52.23s | 1554220 ko | PCUICSafeReduce.vo | 1m51.79s | 1553200 ko || +0m00.43s || 1020 ko | +0.39% | +0.06%
1m11.79s | 2419756 ko | PCUICConfluence.vo | 1m12.41s | 2420136 ko || -0m00.62s || -380 ko | -0.85% | -0.01%
0m50.05s | 1329392 ko | PCUICSafeRetyping.vo | 0m49.37s | 1328380 ko || +0m00.67s || 1012 ko | +1.37% | +0.07%
0m48.12s | 1581644 ko | PCUICSR.vo | 0m48.41s | 1583312 ko || -0m00.28s || -1668 ko | -0.59% | -0.10%
0m47.73s | 1022336 ko | EEtaExpandedFix.vo | 0m47.51s | 1022044 ko || +0m00.21s || 292 ko | +0.46% | +0.02%
0m46.40s | 1245348 ko | PCUICExpandLetsCorrectness.vo | 0m45.87s | 1245448 ko || +0m00.53s || -100 ko | +1.15% | -0.00%
0m41.20s | 1304432 ko | PCUICParallelReduction.vo | 0m41.85s | 1309152 ko || -0m00.64s || -4720 ko | -1.55% | -0.36%
0m38.98s | 1047264 ko | PCUICSigmaCalculus.vo | 0m38.89s | 1046812 ko || +0m00.08s || 452 ko | +0.23% | +0.04%
0m32.62s | 1118676 ko | Conversion/PCUICInstConv.vo | 0m31.85s | 1120584 ko || +0m00.76s || -1908 ko | +2.41% | -0.17%
0m31.10s | 1114448 ko | PCUICInductiveInversion.vo | 0m30.99s | 1111244 ko || +0m00.11s || 3204 ko | +0.35% | +0.28%
0m27.17s | 1110232 ko | PCUICSpine.vo | 0m26.86s | 1110176 ko || +0m00.31s || 56 ko | +1.15% | +0.00%
0m25.95s | 1100860 ko | EWcbvEval.vo | 0m25.73s | 1100976 ko || +0m00.21s || -116 ko | +0.85% | -0.01%
0m24.52s | 1168904 ko | PCUICSafeChecker.vo | 0m24.94s | 1168980 ko || -0m00.42s || -76 ko | -1.68% | -0.00%
0m23.99s | 1265208 ko | ErasureCorrectness.vo | 0m24.46s | 1264596 ko || -0m00.47s || 612 ko | -1.92% | +0.04%
0m22.50s | 1043068 ko | TemplateToPCUICCorrectness.vo | 0m22.24s | 1043052 ko || +0m00.26s || 16 ko | +1.16% | +0.00%
0m22.27s | 1114944 ko | PCUICEquality.vo | 0m21.72s | 1112504 ko || +0m00.55s || 2440 ko | +2.53% | +0.21%
0m21.63s | 984792 ko | ERemoveParams.vo | 0m21.54s | 985820 ko || +0m00.08s || -1028 ko | +0.41% | -0.10%
0m21.41s | 922692 ko | Typing.vo | 0m21.42s | 922792 ko || -0m00.01s || -100 ko | -0.04% | -0.01%
0m19.90s | 992736 ko | PCUICPrincipality.vo | 0m20.79s | 993036 ko || -0m00.89s || -300 ko | -4.28% | -0.03%
0m19.52s | 947280 ko | PCUICWcbvEval.vo | 0m19.61s | 945216 ko || -0m00.08s || 2064 ko | -0.45% | +0.21%
0m19.09s | 927996 ko | PCUICContextConversion.vo | 0m18.66s | 929172 ko || +0m00.42s || -1176 ko | +2.30% | -0.12%
0m18.80s | 900880 ko | PCUICWfUniverses.vo | 0m18.29s | 899852 ko || +0m00.51s || 1028 ko | +2.78% | +0.11%
0m18.06s | 1002184 ko | PCUICTyping.vo | 0m18.18s | 999600 ko || -0m00.12s || 2584 ko | -0.66% | +0.25%
0m17.97s | 913736 ko | Syntax/PCUICOnFreeVars.vo | 0m17.24s | 912672 ko || +0m00.73s || 1064 ko | +4.23% | +0.11%
0m17.52s | 1029036 ko | ErasureProperties.vo | 0m17.51s | 1028488 ko || +0m00.00s || 548 ko | +0.05% | +0.05%
0m17.42s | 1086728 ko | Typed/Erasure.vo | 0m17.37s | 1085240 ko || +0m00.05s || 1488 ko | +0.28% | +0.13%
0m16.97s | 851412 ko | Syntax/PCUICClosed.vo | 0m17.16s | 852008 ko || -0m00.19s || -596 ko | -1.10% | -0.06%
0m16.91s | 1056300 ko | PCUICNormal.vo | 0m16.68s | 1058444 ko || +0m00.23s || -2144 ko | +1.37% | -0.20%
0m16.47s | 1182100 ko | ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo | 0m16.58s | 1186608 ko || -0m00.10s || -4508 ko | -0.66% | -0.37%
0m16.32s | 927268 ko | EtaExpand.vo | 0m15.66s | 927188 ko || +0m00.66s || 80 ko | +4.21% | +0.00%
0m16.13s | 965628 ko | PCUICInductives.vo | 0m15.98s | 968672 ko || +0m00.14s || -3044 ko | +0.93% | -0.31%
0m15.66s | 925032 ko | PCUICSubstitution.vo | 0m14.92s | 924984 ko || +0m00.74s || 48 ko | +4.95% | +0.00%
0m15.47s | 983984 ko | EConstructorsAsBlocks.vo | 0m15.36s | 984812 ko || +0m00.11s || -828 ko | +0.71% | -0.08%
0m14.86s | 1003720 ko | PCUICCumulProp.vo | 0m14.99s | 999676 ko || -0m00.13s || 4044 ko | -0.86% | +0.40%
0m14.71s | 824652 ko | ELiftSubst.vo | 0m14.46s | 823844 ko || +0m00.25s || 808 ko | +1.72% | +0.09%
0m14.48s | 1348108 ko | EWcbvEvalNamed.vo | 0m14.46s | 1348592 ko || +0m00.01s || -484 ko | +0.13% | -0.03%
0m14.46s | 999052 ko | PCUICConvCumInversion.vo | 0m14.24s | 999148 ko || +0m00.22s || -96 ko | +1.54% | -0.00%
0m14.29s | 1034560 ko | Syntax/PCUICPosition.vo | 0m13.91s | 1034840 ko || +0m00.37s || -280 ko | +2.73% | -0.02%
0m13.86s | 837460 ko | UniversesDec.vo | 0m13.23s | 839184 ko || +0m00.62s || -1724 ko | +4.76% | -0.20%
0m13.67s | 878320 ko | EEtaExpanded.vo | 0m13.78s | 878468 ko || -0m00.10s || -148 ko | -0.79% | -0.01%
0m13.65s | 1034068 ko | Bidirectional/BDUnique.vo | 0m13.07s | 1035320 ko || +0m00.58s || -1252 ko | +4.43% | -0.12%
0m13.60s | 1016744 ko | PCUICToTemplateCorrectness.vo | 0m13.63s | 1020824 ko || -0m00.03s || -4080 ko | -0.22% | -0.39%
0m13.12s | 1064192 ko | PCUICEqualityDec.vo | 0m13.21s | 1064180 ko || -0m00.09s || 12 ko | -0.68% | +0.00%
0m12.85s | 860492 ko | Syntax/PCUICLiftSubst.vo | 0m12.31s | 863856 ko || +0m00.53s || -3364 ko | +4.38% | -0.38%
0m12.66s | 965432 ko | PCUICAlpha.vo | 0m12.80s | 966800 ko || -0m00.14s || -1368 ko | -1.09% | -0.14%
0m12.16s | 866212 ko | EWellformed.vo | 0m11.84s | 866092 ko || +0m00.32s || 120 ko | +2.70% | +0.01%
0m11.99s | 620260 ko | wGraph.vo | 0m11.36s | 619948 ko || +0m00.63s || 312 ko | +5.54% | +0.05%
0m11.86s | 954876 ko | ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo | 0m10.90s | 940440 ko || +0m00.95s || 14436 ko | +8.80% | +1.53%
0m11.46s | 811992 ko | LiftSubst.vo | 0m11.28s | 812472 ko || +0m00.18s || -480 ko | +1.59% | -0.05%
0m10.69s | 947604 ko | EOptimizePropDiscr.vo | 0m10.81s | 947568 ko || -0m00.12s || 36 ko | -1.11% | +0.00%
0m10.56s | 906820 ko | Typing/PCUICRenameTyp.vo | 0m10.07s | 907072 ko || +0m00.49s || -252 ko | +4.86% | -0.02%
0m10.39s | 934440 ko | PCUICWellScopedCumulativity.vo | 0m10.07s | 934656 ko || +0m00.32s || -216 ko | +3.17% | -0.02%
0m10.27s | 942596 ko | EWcbvEvalCstrsAsBlocksFixLambdaInd.vo | 0m10.16s | 942940 ko || +0m00.10s || -344 ko | +1.08% | -0.03%
0m09.95s | 920116 ko | ToTemplate/QuotationOf/Common/Environment/Sig.vo | 0m09.20s | 915556 ko || +0m00.75s || 4560 ko | +8.15% | +0.49%
0m09.89s | 932192 ko | PCUICInversion.vo | 0m09.86s | 932188 ko || +0m00.03s || 4 ko | +0.30% | +0.00%
0m09.72s | 995656 ko | Typed/WcbvEvalAux.vo | 0m09.63s | 994256 ko || +0m00.08s || 1400 ko | +0.93% | +0.14%
0m09.20s | 929512 ko | EnvironmentTyping.vo | 0m08.82s | 931124 ko || +0m00.37s || -1612 ko | +4.30% | -0.17%
0m08.96s | 966456 ko | PCUICArities.vo | 0m09.04s | 965500 ko || -0m00.07s || 956 ko | -0.88% | +0.09%
0m08.57s | 894340 ko | Conversion/PCUICNamelessConv.vo | 0m08.50s | 894596 ko || +0m00.07s || -256 ko | +0.82% | -0.02%
0m08.53s | 972256 ko | EDeps.vo | 0m08.92s | 970240 ko || -0m00.39s || 2016 ko | -4.37% | +0.20%
0m08.52s | 947428 ko | ESubstitution.vo | 0m08.59s | 948356 ko || -0m00.07s || -928 ko | -0.81% | -0.09%
0m08.34s | 881252 ko | PCUICContexts.vo | 0m07.88s | 880936 ko || +0m00.46s || 316 ko | +5.83% | +0.03%
0m08.31s | 895884 ko | Conversion/PCUICUnivSubstitutionConv.vo | 0m08.09s | 894428 ko || +0m00.22s || 1456 ko | +2.71% | +0.16%
0m08.30s | 918576 ko | EWcbvEvalEtaInd.vo | 0m08.64s | 915772 ko || -0m00.33s || 2804 ko | -3.93% | +0.30%
0m08.30s | 884536 ko | Typing/PCUICInstTyp.vo | 0m08.34s | 881820 ko || -0m00.03s || 2716 ko | -0.47% | +0.30%
0m08.28s | 933904 ko | EInlineProjections.vo | 0m08.43s | 933400 ko || -0m00.15s || 504 ko | -1.77% | +0.05%
0m08.05s | 943040 ko | PCUICCanonicity.vo | 0m08.15s | 943236 ko || -0m00.09s || -196 ko | -1.22% | -0.02%
0m07.68s | 832784 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo | 0m06.89s | 822552 ko || +0m00.79s || 10232 ko | +11.46% | +1.24%
0m07.46s | 921956 ko | Typing/PCUICWeakeningConfigTyp.vo | 0m07.46s | 920328 ko || +0m00.00s || 1628 ko | +0.00% | +0.17%
0m07.36s | 860768 ko | Typing/PCUICClosedTyp.vo | 0m07.55s | 860912 ko || -0m00.18s || -144 ko | -2.51% | -0.01%
0m07.26s | 881804 ko | times_bool_fun.vo | 0m06.80s | 882624 ko || +0m00.46s || -820 ko | +6.76% | -0.09%
0m07.11s | 906032 ko | Bidirectional/BDStrengthening.vo | 0m07.25s | 906552 ko || -0m00.13s || -520 ko | -1.93% | -0.05%
0m07.08s | 841896 ko | TypingWf.vo | 0m07.13s | 841328 ko || -0m00.04s || 568 ko | -0.70% | +0.06%
0m06.94s | 958420 ko | TemplateToPCUICWcbvEval.vo | 0m07.05s | 955952 ko || -0m00.10s || 2468 ko | -1.56% | +0.25%
0m06.86s | 821504 ko | Syntax/PCUICUnivSubst.vo | 0m06.80s | 820692 ko || +0m00.06s || 812 ko | +0.88% | +0.09%
0m06.80s | 934628 ko | PCUICElimination.vo | 0m07.23s | 934172 ko || -0m00.43s || 456 ko | -5.94% | +0.04%
0m06.75s | 892964 ko | PCUICCasesHelper.vo | 0m06.67s | 892816 ko || +0m00.08s || 148 ko | +1.19% | +0.01%
0m06.58s | 1113144 ko | ToTemplate/Coq/MSets.vo | 0m06.01s | 1076552 ko || +0m00.57s || 36592 ko | +9.48% | +3.39%
0m06.57s | 527096 ko | All_Forall.vo | 0m06.37s | 527668 ko || +0m00.20s || -572 ko | +3.13% | -0.10%
0m06.33s | 919488 ko | EArities.vo | 0m06.42s | 922716 ko || -0m00.08s || -3228 ko | -1.40% | -0.34%
0m06.24s | 841360 ko | ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo | 0m06.10s | 848544 ko || +0m00.14s || -7184 ko | +2.29% | -0.84%
0m05.90s | 894784 ko | PCUICEtaExpand.vo | 0m05.99s | 894648 ko || -0m00.08s || 136 ko | -1.50% | +0.01%
0m05.73s | 894636 ko | Typing/PCUICContextConversionTyp.vo | 0m05.83s | 889988 ko || -0m00.09s || 4648 ko | -1.71% | +0.52%
0m05.60s | 818316 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo | 0m05.04s | 827232 ko || +0m00.55s || -8916 ko | +11.11% | -1.07%
0m05.40s | 853160 ko | Conversion/PCUICOnFreeVarsConv.vo | 0m05.24s | 853176 ko || +0m00.16s || -16 ko | +3.05% | -0.00%
0m05.31s | 890188 ko | EWcbvEvalCstrsAsBlocksInd.vo | 0m05.09s | 888856 ko || +0m00.21s || 1332 ko | +4.32% | +0.14%
0m05.28s | 863400 ko | Typing/PCUICUnivSubstitutionTyp.vo | 0m05.64s | 862668 ko || -0m00.35s || 732 ko | -6.38% | +0.08%
0m05.24s | 774532 ko | Universes.vo | 0m05.26s | 774668 ko || -0m00.01s || -136 ko | -0.38% | -0.01%
0m05.21s | 901132 ko | ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo | 0m05.16s | 890940 ko || +0m00.04s || 10192 ko | +0.96% | +1.14%
0m05.20s | 783880 ko | WcbvEval.vo | 0m05.21s | 785540 ko || -0m00.00s || -1660 ko | -0.19% | -0.21%
0m05.19s | 855116 ko | Bidirectional/BDTyping.vo | 0m05.26s | 850480 ko || -0m00.06s || 4636 ko | -1.33% | +0.54%
0m05.17s | 906096 ko | PCUICFirstorder.vo | 0m05.19s | 906676 ko || -0m00.02s || -580 ko | -0.38% | -0.06%
0m05.12s | 914600 ko | PCUICProgress.vo | 0m05.13s | 915224 ko || -0m00.00s || -624 ko | -0.19% | -0.06%
0m05.11s | 844812 ko | PCUICReduction.vo | 0m05.05s | 844324 ko || +0m00.06s || 488 ko | +1.18% | +0.05%
0m05.00s | 872084 ko | PCUICContextReduction.vo | 0m05.01s | 870408 ko || -0m00.00s || 1676 ko | -0.19% | +0.19%
0m04.94s | 779368 ko | TermEquality.vo | 0m04.96s | 780648 ko || -0m00.01s || -1280 ko | -0.40% | -0.16%
0m04.92s | 918480 ko | TemplateToPCUICExpanded.vo | 0m04.71s | 918332 ko || +0m00.20s || 148 ko | +4.45% | +0.01%
0m04.73s | 903548 ko | ToTemplate/Coq/FSets.vo | 0m03.88s | 901912 ko || +0m00.85s || 1636 ko | +21.90% | +0.18%
0m04.68s | 783620 ko | PCUICAst.vo | 0m04.64s | 784380 ko || +0m00.04s || -760 ko | +0.86% | -0.09%
0m04.66s | 736332 ko | Environment.vo | 0m04.48s | 735356 ko || +0m00.17s || 976 ko | +4.01% | +0.13%
0m04.53s | 821968 ko | ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo | 0m04.24s | 829116 ko || +0m00.29s || -7148 ko | +6.83% | -0.86%
0m04.53s | 863240 ko | ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo | 0m04.45s | 861816 ko || +0m00.08s || 1424 ko | +1.79% | +0.16%
0m04.51s | 960120 ko | ToTemplate/Common/Universes.vo | 0m04.02s | 961812 ko || +0m00.49s || -1692 ko | +12.18% | -0.17%
0m04.41s | 892628 ko | Bidirectional/BDToPCUIC.vo | 0m04.27s | 892628 ko || +0m00.14s || 0 ko | +3.27% | +0.00%
0m04.41s | 849932 ko | Conversion/PCUICWeakeningEnvConv.vo | 0m04.10s | 850004 ko || +0m00.31s || -72 ko | +7.56% | -0.00%
0m04.37s | 912276 ko | PCUICSafeLemmata.vo | 0m04.48s | 914012 ko || -0m00.11s || -1736 ko | -2.45% | -0.18%
0m04.37s | 1044468 ko | Typed/ErasureCorrectness.vo | 0m04.35s | 1044608 ko || +0m00.02s || -140 ko | +0.45% | -0.01%
0m04.29s | 1062988 ko | Extraction.vo | 0m04.26s | 1063612 ko || +0m00.03s || -624 ko | +0.70% | -0.05%
0m04.29s | 727200 ko | Kernames.vo | 0m04.47s | 729924 ko || -0m00.17s || -2724 ko | -4.02% | -0.37%
0m04.22s | 893696 ko | PCUICValidity.vo | 0m04.35s | 892668 ko || -0m00.12s || 1028 ko | -2.98% | +0.11%
0m04.14s | 770328 ko | UnivSubst.vo | 0m04.90s | 769344 ko || -0m00.76s || 984 ko | -15.51% | +0.12%
0m04.11s | 823284 ko | ReflectAst.vo | 0m05.10s | 821492 ko || -0m00.98s || 1792 ko | -19.41% | +0.21%
0m04.10s | 922912 ko | EGenericMapEnv.vo | 0m04.14s | 921080 ko || -0m00.04s || 1832 ko | -0.96% | +0.19%
0m04.08s | 892140 ko | Bidirectional/BDFromPCUIC.vo | 0m03.96s | 892356 ko || +0m00.12s || -216 ko | +3.03% | -0.02%
0m04.07s | 848564 ko | Typing/PCUICWeakeningEnvTyp.vo | 0m03.66s | 848476 ko || +0m00.41s || 88 ko | +11.20% | +0.01%
0m04.05s | 845280 ko | Syntax/PCUICReflect.vo | 0m04.03s | 844008 ko || +0m00.01s || 1272 ko | +0.49% | +0.15%
0m03.93s | 812692 ko | ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo | 0m03.83s | 819012 ko || +0m00.10s || -6320 ko | +2.61% | -0.77%
0m03.84s | 911188 ko | param_generous_packed.vo | 0m03.90s | 916344 ko || -0m00.06s || -5156 ko | -1.53% | -0.56%
0m03.71s | 920876 ko | PCUICWfReduction.vo | 0m03.84s | 921144 ko || -0m00.12s || -268 ko | -3.38% | -0.02%
0m03.65s | 824952 ko | utils/PCUICAstUtils.vo | 0m03.65s | 823420 ko || +0m00.00s || 1532 ko | +0.00% | +0.18%
0m03.64s | 910484 ko | PCUICWfEnvImpl.vo | 0m03.66s | 910424 ko || -0m00.02s || 60 ko | -0.54% | +0.00%
0m03.64s | 782192 ko | WfAst.vo | 0m04.01s | 780548 ko || -0m00.36s || 1644 ko | -9.22% | +0.21%
0m03.61s | 809972 ko | ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo | 0m03.75s | 815048 ko || -0m00.14s || -5076 ko | -3.73% | -0.62%
0m03.60s | 851360 ko | Checker.vo | 0m03.67s | 852148 ko || -0m00.06s || -788 ko | -1.90% | -0.09%
0m03.55s | 803224 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo | 0m03.30s | 802232 ko || +0m00.25s || 992 ko | +7.57% | +0.12%
0m03.52s | 818516 ko | Syntax/PCUICDepth.vo | 0m03.46s | 817568 ko || +0m00.06s || 948 ko | +1.73% | +0.11%
0m03.49s | 833484 ko | ToTemplate/QuotationOf/Utils/MCMSets/Sig.vo | 0m03.68s | 832740 ko || -0m00.18s || 744 ko | -5.16% | +0.08%
0m03.45s | 845884 ko | Conversion/PCUICWeakeningConfigConv.vo | 0m03.28s | 843928 ko || +0m00.17s || 1956 ko | +5.18% | +0.23%
0m03.44s | 810052 ko | ToTemplate/Coq/Init.vo | 0m02.92s | 807396 ko || +0m00.52s || 2656 ko | +17.80% | +0.32%
0m03.43s | 910028 ko | PCUICWfEnv.vo | 0m03.41s | 911392 ko || +0m00.02s || -1364 ko | +0.58% | -0.14%
0m03.40s | 824912 ko | Syntax/PCUICInduction.vo | 0m03.41s | 825424 ko || -0m00.01s || -512 ko | -0.29% | -0.06%
0m03.33s | 851964 ko | PCUICRedTypeIrrelevance.vo | 0m03.36s | 851668 ko || -0m00.02s || 296 ko | -0.89% | +0.03%
0m03.33s | 837152 ko | times_bool_fun2.vo | 0m03.42s | 836444 ko || -0m00.08s || 708 ko | -2.63% | +0.08%
0m03.32s | 867724 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo | 0m03.46s | 867584 ko || -0m00.14s || 140 ko | -4.04% | +0.01%
0m03.27s | 830628 ko | Typed/ClosedAux.vo | 0m03.35s | 829380 ko || -0m00.08s || 1248 ko | -2.38% | +0.15%
0m03.16s | 776476 ko | EInduction.vo | 0m03.10s | 775856 ko || +0m00.06s || 620 ko | +1.93% | +0.07%
0m03.11s | 853220 ko | ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo | 0m03.03s | 850768 ko || +0m00.08s || 2452 ko | +2.64% | +0.28%
0m03.00s | 822588 ko | ToTemplate/QuotationOf/Utils/MCFSets/Sig.vo | 0m03.06s | 823584 ko || -0m00.06s || -996 ko | -1.96% | -0.12%
0m02.90s | 920260 ko | Prelim.vo | 0m02.98s | 923452 ko || -0m00.08s || -3192 ko | -2.68% | -0.34%
0m02.89s | 792216 ko | EReflect.vo | 0m02.90s | 790940 ko || -0m00.00s || 1276 ko | -0.34% | +0.16%
0m02.88s | 838560 ko | PCUICCumulativitySpec.vo | 0m02.80s | 839404 ko || +0m00.08s || -844 ko | +2.85% | -0.10%
0m02.81s | 804472 ko | ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo | 0m02.69s | 804048 ko || +0m00.12s || 424 ko | +4.46% | +0.05%
0m02.79s | 735800 ko | Reflect.vo | 0m02.75s | 736872 ko || +0m00.04s || -1072 ko | +1.45% | -0.14%
0m02.79s | 817792 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraDecide/Instances.vo | 0m02.45s | 820280 ko || +0m00.33s || -2488 ko | +13.87% | -0.30%
0m02.79s | 798960 ko | ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo | 0m02.76s | 800356 ko || +0m00.03s || -1396 ko | +1.08% | -0.17%
0m02.75s | 820112 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapDecide/Instances.vo | 0m02.74s | 822600 ko || +0m00.00s || -2488 ko | +0.36% | -0.30%
0m02.71s | 1039492 ko | SafeTemplateChecker.vo | 0m02.74s | 1038752 ko || -0m00.03s || 740 ko | -1.09% | +0.07%
0m02.66s | 1056696 ko | ToTemplate/Template/Ast.vo | 0m02.60s | 1056880 ko || +0m00.06s || -184 ko | +2.30% | -0.01%
0m02.65s | 819708 ko | Syntax/PCUICCases.vo | 0m02.64s | 824128 ko || +0m00.00s || -4420 ko | +0.37% | -0.53%
0m02.58s | 947292 ko | Typed/CertifyingInlining.vo | 0m02.67s | 947884 ko || -0m00.08s || -592 ko | -3.37% | -0.06%
0m02.57s | 828372 ko | PCUICContextSubst.vo | 0m02.46s | 827776 ko || +0m00.10s || 596 ko | +4.47% | +0.07%
0m02.55s | 945696 ko | Typed/CertifyingBeta.vo | 0m02.57s | 946312 ko || -0m00.02s || -616 ko | -0.77% | -0.06%
0m02.48s | 852488 ko | EWcbvEvalInd.vo | 0m02.32s | 852264 ko || +0m00.16s || 224 ko | +6.89% | +0.02%
0m02.46s | 841304 ko | translation_utils.vo | 0m02.48s | 843552 ko || -0m00.02s || -2248 ko | -0.80% | -0.26%
0m02.43s | 687872 ko | BasicAst.vo | 0m02.31s | 688672 ko || +0m00.12s || -800 ko | +5.19% | -0.11%
0m02.41s | 906244 ko | PCUICNormalization.vo | 0m02.36s | 907128 ko || +0m00.05s || -884 ko | +2.11% | -0.09%
0m02.41s | 934364 ko | ToTemplate/Common/Kernames.vo | 0m02.53s | 932184 ko || -0m00.11s || 2180 ko | -4.74% | +0.23%
0m02.40s | 853032 ko | Conversion/PCUICWeakeningConv.vo | 0m02.39s | 852692 ko || +0m00.00s || 340 ko | +0.41% | +0.03%
0m02.38s | 956236 ko | PCUICTransform.vo | 0m02.45s | 956644 ko || -0m00.07s || -408 ko | -2.85% | -0.04%
0m02.37s | 801120 ko | ToTemplate/Utils/All_Forall.vo | 0m01.94s | 801828 ko || +0m00.43s || -708 ko | +22.16% | -0.08%
0m02.36s | 822124 ko | Syntax/PCUICViews.vo | 0m02.34s | 822132 ko || +0m00.02s || -8 ko | +0.85% | -0.00%
0m02.34s | 900632 ko | Extract.vo | 0m02.35s | 901388 ko || -0m00.01s || -756 ko | -0.42% | -0.08%
0m02.34s | 820292 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetExtraDecide/Instances.vo | 0m02.37s | 822312 ko || -0m00.03s || -2020 ko | -1.26% | -0.24%
0m02.32s | 827228 ko | PCUICErrors.vo | 0m02.49s | 827348 ko || -0m00.17s || -120 ko | -6.82% | -0.01%
0m02.32s | 818804 ko | ToTemplate/Init.vo | 0m02.02s | 816280 ko || +0m00.29s || 2524 ko | +14.85% | +0.30%
0m02.32s | 820452 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraDecide/Instances.vo | 0m02.22s | 821096 ko || +0m00.09s || -644 ko | +4.50% | -0.07%
0m02.32s | 800816 ko | ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo | 0m02.04s | 804060 ko || +0m00.27s || -3244 ko | +13.72% | -0.40%
0m02.29s | 972612 ko | ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo | 0m02.27s | 973124 ko || +0m00.02s || -512 ko | +0.88% | -0.05%
0m02.27s | 633640 ko | MCFSets.vo | 0m02.15s | 633424 ko || +0m00.12s || 216 ko | +5.58% | +0.03%
0m02.27s | 841932 ko | PCUICCumulativity.vo | 0m02.32s | 841096 ko || -0m00.04s || 836 ko | -2.15% | +0.09%
0m02.27s | 944948 ko | Typed/Optimize.vo | 0m02.34s | 945264 ko || -0m00.06s || -316 ko | -2.99% | -0.03%
0m02.22s | 938368 ko | Typed/Annotations.vo | 0m02.17s | 938824 ko || +0m00.05s || -456 ko | +2.30% | -0.04%
0m02.21s | 897268 ko | PCUICSN.vo | 0m02.24s | 896764 ko || -0m00.03s || 504 ko | -1.33% | +0.05%
0m02.20s | 842116 ko | PCUICWeakeningEnv.vo | 0m02.39s | 842780 ko || -0m00.18s || -664 ko | -7.94% | -0.07%
0m02.17s | 363628 ko | MiniHoTT.vo | 0m02.05s | 359728 ko || +0m00.12s || 3900 ko | +5.85% | +1.08%
0m02.17s | 918680 ko | Typed/OptimizePropDiscr.vo | 0m02.14s | 918536 ko || +0m00.02s || 144 ko | +1.40% | +0.01%
0m02.14s | 842556 ko | PCUICCSubst.vo | 0m02.16s | 842540 ko || -0m00.02s || 16 ko | -0.92% | +0.00%
0m02.14s | 903320 ko | PCUICConsistency.vo | 0m02.18s | 904636 ko || -0m00.04s || -1316 ko | -1.83% | -0.14%
0m02.14s | 832348 ko | TemplateCheckWf.vo | 0m01.84s | 831408 ko || +0m00.30s || 940 ko | +16.30% | +0.11%
0m02.14s | 805800 ko | ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo | 0m02.11s | 806120 ko || +0m00.03s || -320 ko | +1.42% | -0.03%
0m02.10s | 452984 ko | MCList.vo | 0m01.91s | 454648 ko || +0m00.19s || -1664 ko | +9.94% | -0.36%
0m02.10s | 939524 ko | Typed/Transform.vo | 0m01.99s | 940004 ko || +0m00.11s || -480 ko | +5.52% | -0.05%
0m02.09s | 821496 ko | PCUICCasesContexts.vo | 0m02.02s | 822196 ko || +0m00.06s || -700 ko | +3.46% | -0.08%
0m02.07s | 1064500 ko | ToTemplate/All.vo | 0m01.97s | 1063376 ko || +0m00.09s || 1124 ko | +5.07% | +0.10%
0m02.07s | 774820 ko | utils/PCUICOnOne.vo | 0m01.82s | 774344 ko || +0m00.24s || 476 ko | +13.73% | +0.06%
0m02.06s | 812456 ko | CommonUtils.vo | 0m02.05s | 812336 ko || +0m00.01s || 120 ko | +0.48% | +0.01%
0m02.06s | 894472 ko | PCUICWeakeningEnvSN.vo | 0m02.00s | 896056 ko || +0m00.06s || -1584 ko | +3.00% | -0.17%
0m02.06s | 1057784 ko | ToTemplate/Template/TypingWf.vo | 0m01.97s | 1056860 ko || +0m00.09s || 924 ko | +4.56% | +0.08%
0m02.04s | 863724 ko | ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo | 0m02.09s | 864196 ko || -0m00.04s || -472 ko | -2.39% | -0.05%
0m02.01s | 775680 ko | EnvMap.vo | 0m02.49s | 776568 ko || -0m00.48s || -888 ko | -19.27% | -0.11%
0m02.01s | 360548 ko | MiniHoTT_paths.vo | 0m02.12s | 360628 ko || -0m00.11s || -80 ko | -5.18% | -0.02%
0m02.00s | 861100 ko | ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo | 0m01.90s | 861460 ko || +0m00.10s || -360 ko | +5.26% | -0.04%
0m02.00s | 853840 ko | Typing/PCUICWeakeningTyp.vo | 0m01.84s | 853116 ko || +0m00.15s || 724 ko | +8.69% | +0.08%
0m01.99s | 825788 ko | param_original.vo | 0m01.90s | 824892 ko || +0m00.09s || 896 ko | +4.73% | +0.10%
0m01.97s | 776900 ko | Reduction.vo | 0m01.74s | 779536 ko || +0m00.23s || -2636 ko | +13.21% | -0.33%
0m01.97s | 806596 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo | 0m02.14s | 805556 ko || -0m00.17s || 1040 ko | -7.94% | +0.12%
0m01.96s | 818060 ko | PCUICToTemplate.vo | 0m02.02s | 819568 ko || -0m00.06s || -1508 ko | -2.97% | -0.18%
0m01.95s | 801908 ko | ToTemplate/Utils/MCOption.vo | 0m01.59s | 800856 ko || +0m00.35s || 1052 ko | +22.64% | +0.13%
0m01.94s | 895680 ko | PCUICWeakeningConfigSN.vo | 0m01.99s | 894836 ko || -0m00.05s || 844 ko | -2.51% | +0.09%
0m01.93s | 839884 ko | Conversion/PCUICClosedConv.vo | 0m02.11s | 840164 ko || -0m00.17s || -280 ko | -8.53% | -0.03%
0m01.93s | 801068 ko | ToTemplate/Utils/MCProd.vo | 0m01.80s | 798820 ko || +0m00.12s || 2248 ko | +7.22% | +0.28%
0m01.92s | 766628 ko | EAstUtils.vo | 0m01.66s | 766540 ko || +0m00.26s || 88 ko | +15.66% | +0.01%
0m01.91s | 771324 ko | AstUtils.vo | 0m02.10s | 771088 ko || -0m00.19s || 236 ko | -9.04% | +0.03%
0m01.91s | 1046324 ko | ToTemplate/Template/AstUtils.vo | 0m01.86s | 1047320 ko || +0m00.04s || -996 ko | +2.68% | -0.09%
0m01.90s | 857172 ko | TemplateToPCUIC.vo | 0m01.85s | 856128 ko || +0m00.04s || 1044 ko | +2.70% | +0.12%
0m01.89s | 827596 ko | param_binary.vo | 0m01.93s | 824020 ko || -0m00.04s || 3576 ko | -2.07% | +0.43%
0m01.87s | 935976 ko | ToTemplate/Common/BasicAst.vo | 0m01.86s | 937236 ko || +0m00.01s || -1260 ko | +0.53% | -0.13%
0m01.87s | 808224 ko | ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo | 0m01.99s | 806912 ko || -0m00.11s || 1312 ko | -6.03% | +0.16%
0m01.85s | 802992 ko | ToTemplate/Coq/Numbers.vo | 0m01.61s | 801304 ko || +0m00.24s || 1688 ko | +14.90% | +0.21%
0m01.85s | 827872 ko | Typed/Utils.vo | 0m01.87s | 829816 ko || -0m00.02s || -1944 ko | -1.06% | -0.23%
0m01.82s | 829288 ko | Typed/Certifying.vo | 0m01.84s | 830952 ko || -0m00.02s || -1664 ko | -1.08% | -0.20%
0m01.80s | 805532 ko | ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo | 0m01.77s | 806420 ko || +0m00.03s || -888 ko | +1.69% | -0.11%
0m01.79s | 1015136 ko | ToTemplate/QuotationOf/Template/Ast/Instances.vo | 0m01.80s | 1015804 ko || -0m00.01s || -668 ko | -0.55% | -0.06%
0m01.78s | 775060 ko | EAst.vo | 0m01.81s | 774280 ko || -0m00.03s || 780 ko | -1.65% | +0.10%
0m01.76s | 835984 ko | Syntax/PCUICInstDef.vo | 0m01.74s | 836472 ko || +0m00.02s || -488 ko | +1.14% | -0.05%
0m01.76s | 805564 ko | ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo | 0m01.83s | 805328 ko || -0m00.07s || 236 ko | -3.82% | +0.02%
0m01.75s | 816464 ko | ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo | 0m01.74s | 816532 ko || +0m00.01s || -68 ko | +0.57% | -0.00%
0m01.75s | 102800 ko | gen-src/typing0.cmx | 0m01.37s | 101808 ko || +0m00.37s || 992 ko | +27.73% | +0.97%
0m01.73s | 855344 ko | TemplateMonadToPCUIC.vo | 0m01.75s | 852844 ko || -0m00.02s || 2500 ko | -1.14% | +0.29%
0m01.71s | 821084 ko | Syntax/PCUICTactics.vo | 0m01.80s | 819320 ko || -0m00.09s || 1764 ko | -5.00% | +0.21%
0m01.70s | 832400 ko | PCUICGeneration.vo | 0m01.65s | 832760 ko || +0m00.05s || -360 ko | +3.03% | -0.04%
0m01.69s | 767724 ko | ECSubst.vo | 0m01.72s | 768096 ko || -0m00.03s || -372 ko | -1.74% | -0.04%
0m01.69s | 858804 ko | PCUICTemplateMonad/Core.vo | 0m01.70s | 858764 ko || -0m00.01s || 40 ko | -0.58% | +0.00%
0m01.69s | 823964 ko | param_cheap_packed.vo | 0m01.64s | 823280 ko || +0m00.05s || 684 ko | +3.04% | +0.08%
0m01.68s | 533576 ko | MCMSets.vo | 0m01.48s | 533696 ko || +0m00.19s || -120 ko | +13.51% | -0.02%
0m01.68s | 840908 ko | PCUICTemplateMonad.vo | 0m01.62s | 841660 ko || +0m00.05s || -752 ko | +3.70% | -0.08%
0m01.67s | 861788 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo | 0m01.63s | 861476 ko || +0m00.04s || 312 ko | +2.45% | +0.03%
0m01.66s | 837352 ko | PCUICGlobalEnv.vo | 0m01.69s | 836376 ko || -0m00.03s || 976 ko | -1.77% | +0.11%
0m01.66s | 802668 ko | ToTemplate/Coq/Lists.vo | 0m01.43s | 801872 ko || +0m00.23s || 796 ko | +16.08% | +0.09%
0m01.66s | 814952 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetExtraOrdProp/Instances.vo | 0m01.56s | 814500 ko || +0m00.09s || 452 ko | +6.41% | +0.05%
0m01.65s | 799364 ko | ToTemplate/Coq/ssr.vo | 0m01.41s | 800256 ko || +0m00.24s || -892 ko | +17.02% | -0.11%
0m01.64s | 817500 ko | EEnvMap.vo | 0m01.63s | 818800 ko || +0m00.01s || -1300 ko | +0.61% | -0.15%
0m01.64s | 826328 ko | PCUICWeakeningConfig.vo | 0m01.62s | 827336 ko || +0m00.01s || -1008 ko | +1.23% | -0.12%
0m01.63s | 813220 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetExtraOrdProp/Instances.vo | 0m01.73s | 815188 ko || -0m00.10s || -1968 ko | -5.78% | -0.24%
0m01.63s | 89764 ko | gen-src/metacoq_template_plugin.cmxs | 0m01.32s | 89836 ko || +0m00.30s || -72 ko | +23.48% | -0.08%
0m01.62s | 831348 ko | PCUICExpandLets.vo | 0m01.51s | 832060 ko || +0m00.11s || -712 ko | +7.28% | -0.08%
0m01.62s | 834716 ko | PCUICProgram.vo | 0m01.49s | 834740 ko || +0m00.13s || -24 ko | +8.72% | -0.00%
0m01.62s | 810940 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetExtraOrdProp/Instances.vo | 0m01.63s | 810504 ko || -0m00.00s || 436 ko | -0.61% | +0.05%
0m01.62s | 799068 ko | ToTemplate/Utils/MCReflect.vo | 0m01.47s | 799612 ko || +0m00.15s || -544 ko | +10.20% | -0.06%
0m01.62s | 765756 ko | utils/PCUICPrimitive.vo | 0m01.57s | 766036 ko || +0m00.05s || -280 ko | +3.18% | -0.03%
0m01.60s | 831228 ko | Syntax/PCUICRenameDef.vo | 0m01.74s | 831412 ko || -0m00.13s || -184 ko | -8.04% | -0.02%
0m01.60s | 798132 ko | ToTemplate/Common/Primitive.vo | 0m01.52s | 799156 ko || +0m00.08s || -1024 ko | +5.26% | -0.12%
0m01.58s | 814716 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetExtraOrdProp/Instances.vo | 0m01.68s | 814024 ko || -0m00.09s || 692 ko | -5.95% | +0.08%
0m01.56s | 820584 ko | All.vo | 0m01.64s | 819396 ko || -0m00.07s || 1188 ko | -4.87% | +0.14%
0m01.55s | 799148 ko | ToTemplate/Utils/MCList.vo | 0m01.56s | 798348 ko || -0m00.01s || 800 ko | -0.64% | +0.10%
0m01.54s | 798112 ko | ToTemplate/Utils/bytestring.vo | 0m01.56s | 798592 ko || -0m00.02s || -480 ko | -1.28% | -0.06%
0m01.53s | 810988 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo | 0m01.53s | 810968 ko || +0m00.00s || 20 ko | +0.00% | +0.00%
0m01.52s | 823240 ko | TemplateEnvMap.vo | 0m01.64s | 823500 ko || -0m00.11s || -260 ko | -7.31% | -0.03%
0m01.52s | 811556 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo | 0m01.59s | 811208 ko || -0m00.07s || 348 ko | -4.40% | +0.04%
0m01.51s | 807716 ko | ToTemplate/Utils/utils.vo | 0m01.54s | 806820 ko || -0m00.03s || 896 ko | -1.94% | +0.11%
0m01.49s | 820368 ko | EExtends.vo | 0m01.51s | 821928 ko || -0m00.02s || -1560 ko | -1.32% | -0.18%
0m01.48s | 804264 ko | ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo | 0m01.43s | 804068 ko || +0m00.05s || 196 ko | +3.49% | +0.02%
0m01.46s | 770792 ko | Ast.vo | 0m01.68s | 770956 ko || -0m00.21s || -164 ko | -13.09% | -0.02%
0m01.45s | 874796 ko | Typing/PCUICNamelessTyp.vo | 0m01.47s | 874812 ko || -0m00.02s || -16 ko | -1.36% | -0.00%
0m01.44s | 798808 ko | ToTemplate/Coq/Bool.vo | 0m01.58s | 799452 ko || -0m00.14s || -644 ko | -8.86% | -0.08%
0m01.43s | 801932 ko | Constants.vo | 0m01.55s | 802112 ko || -0m00.12s || -180 ko | -7.74% | -0.02%
0m01.43s | 798132 ko | ToTemplate/Utils/MCArith.vo | 0m01.30s | 797944 ko || +0m00.12s || 188 ko | +9.99% | +0.02%
0m01.41s | 817020 ko | ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo | 0m01.35s | 816940 ko || +0m00.05s || 80 ko | +4.44% | +0.00%
0m01.40s | 868848 ko | ToTemplate/QuotationOf/Common/Kernames/Instances.vo | 0m01.43s | 867412 ko || -0m00.03s || 1436 ko | -2.09% | +0.16%
0m01.40s | 800204 ko | ToTemplate/Utils/MCUtils.vo | 0m01.39s | 799832 ko || +0m00.01s || 372 ko | +0.71% | +0.04%
0m01.40s | 822712 ko | standard_model.vo | 0m01.43s | 822520 ko || -0m00.03s || 192 ko | -2.09% | +0.02%
0m01.39s | 850328 ko | ToTemplate/QuotationOf/Common/Universes/Instances.vo | 0m01.35s | 847584 ko || +0m00.03s || 2744 ko | +2.96% | +0.32%
0m01.39s | 859096 ko | ToTemplate/QuotationOf/Template/Typing/Instances.vo | 0m01.40s | 860304 ko || -0m00.01s || -1208 ko | -0.71% | -0.14%
0m01.39s | 433540 ko | canonicaltries/CanonicalTries.vo | 0m01.12s | 433428 ko || +0m00.26s || 112 ko | +24.10% | +0.02%
0m01.39s | 769428 ko | utils/PCUICSize.vo | 0m01.05s | 770352 ko || +0m00.33s || -924 ko | +32.38% | -0.11%
0m01.38s | 833748 ko | PCUICGuardCondition.vo | 0m01.34s | 832652 ko || +0m00.03s || 1096 ko | +2.98% | +0.13%
0m01.38s | 799788 ko | ToTemplate/Utils/ReflectEq.vo | 0m01.53s | 798212 ko || -0m00.15s || 1576 ko | -9.80% | +0.19%
0m01.34s | 770404 ko | EGlobalEnv.vo | 0m01.32s | 770392 ko || +0m00.02s || 12 ko | +1.51% | +0.00%
0m01.34s | 799112 ko | ToTemplate/Coq/Strings.vo | 0m01.29s | 799124 ko || +0m00.05s || -12 ko | +3.87% | -0.00%
0m01.34s | 817896 ko | sigma.vo | 0m01.46s | 817992 ko || -0m00.11s || -96 ko | -8.21% | -0.01%
0m01.34s | 809816 ko | utils/PCUICPretty.vo | 0m01.24s | 811240 ko || +0m00.10s || -1424 ko | +8.06% | -0.17%
0m01.33s | 798924 ko | ToTemplate/Common/config.vo | 0m01.44s | 798768 ko || -0m00.10s || 156 ko | -7.63% | +0.01%
0m01.32s | 777256 ko | ESpineView.vo | 0m01.42s | 775508 ko || -0m00.09s || 1748 ko | -7.04% | +0.22%
0m01.31s | 829424 ko | Syntax/PCUICNamelessDef.vo | 0m01.33s | 830048 ko || -0m00.02s || -624 ko | -1.50% | -0.07%
0m01.29s | 843928 ko | EProgram.vo | 0m01.43s | 844976 ko || -0m00.13s || -1048 ko | -9.79% | -0.12%
0m01.27s | 809544 ko | ToTemplate/Coq/Floats.vo | 0m01.36s | 809740 ko || -0m00.09s || -196 ko | -6.61% | -0.02%
0m01.26s | 809928 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapExtraFact/Instances.vo | 0m01.34s | 810692 ko || -0m00.08s || -764 ko | -5.97% | -0.09%
0m01.24s | 819324 ko | TemplateProgram.vo | 0m01.24s | 819744 ko || +0m00.00s || -420 ko | +0.00% | -0.05%
0m01.21s | 766624 ko | Pretty.vo | 0m01.19s | 766580 ko || +0m00.02s || 44 ko | +1.68% | +0.00%
0m01.20s | 764756 ko | TemplateMonad/Core.vo | 0m01.29s | 765168 ko || -0m00.09s || -412 ko | -6.97% | -0.05%
0m01.17s | 763876 ko | TemplateMonad/Extractable.vo | 0m01.13s | 763624 ko || +0m00.04s || 252 ko | +3.53% | +0.03%
0m01.13s | 762384 ko | MonadAst.vo | 0m01.15s | 762548 ko || -0m00.02s || -164 ko | -1.73% | -0.02%
0m01.12s | 769344 ko | Typed/ExAst.vo | 0m01.13s | 770056 ko || -0m00.00s || -712 ko | -0.88% | -0.09%
0m01.11s | 775004 ko | Normal.vo | 0m01.11s | 774644 ko || +0m00.00s || 360 ko | +0.00% | +0.04%
0m01.10s | 772256 ko | EPretty.vo | 0m01.20s | 770688 ko || -0m00.09s || 1568 ko | -8.33% | +0.20%
0m01.10s | 761084 ko | TemplateMonad/Common.vo | 0m00.97s | 762364 ko || +0m00.13s || -1280 ko | +13.40% | -0.16%
0m01.09s | 763304 ko | Induction.vo | 0m01.34s | 763428 ko || -0m00.25s || -124 ko | -18.65% | -0.01%
0m01.08s | 752576 ko | TemplateMonad.vo | 0m01.23s | 753836 ko || -0m00.14s || -1260 ko | -12.19% | -0.16%
0m01.03s | 767512 ko | PCUICMonadAst.vo | 0m01.04s | 766860 ko || -0m00.01s || 652 ko | -0.96% | +0.08%
0m00.99s | 217328 ko | gen-src/metacoq_template_plugin.cmx | 0m00.93s | 217300 ko || +0m00.05s || 28 ko | +6.45% | +0.01%
0m00.94s | 53112 ko | gen-src/byte.cmx | 0m00.75s | 53164 ko || +0m00.18s || -52 ko | +25.33% | -0.09%
0m00.92s | 678120 ko | MonadBasicAst.vo | 0m00.83s | 677604 ko || +0m00.09s || 516 ko | +10.84% | +0.07%
0m00.87s | 99152 ko | gen-src/environmentTyping.cmx | 0m00.71s | 97500 ko || +0m00.16s || 1652 ko | +22.53% | +1.69%
0m00.83s | 131532 ko | gen-src/fMapAVL.cmi | 0m00.66s | 131284 ko || +0m00.16s || 248 ko | +25.75% | +0.18%
0m00.71s | 92312 ko | gen-src/fMapAVL.cmx | 0m00.51s | 92304 ko || +0m00.19s || 8 ko | +39.21% | +0.00%
0m00.67s | 73048 ko | gen-src/byte0.cmx | 0m00.47s | 72844 ko || +0m00.20s || 204 ko | +42.55% | +0.28%
0m00.64s | 422780 ko | config.vo | 0m00.64s | 423208 ko || +0m00.00s || -428 ko | +0.00% | -0.10%
0m00.64s | 55492 ko | gen-src/all_Forall.cmx | 0m00.50s | 55460 ko || +0m00.14s || 32 ko | +28.00% | +0.05%
0m00.55s | 441128 ko | monad_utils.vo | 0m00.40s | 441532 ko || +0m00.15s || -404 ko | +37.50% | -0.09%
0m00.55s | 510188 ko | utils/PCUICUtils.vo | 0m00.56s | 509772 ko || -0m00.01s || 416 ko | -1.78% | +0.08%
0m00.53s | 98196 ko | gen-src/kernames.cmx | 0m00.44s | 98860 ko || +0m00.09s || -664 ko | +20.45% | -0.67%
0m00.49s | 85360 ko | gen-src/environmentTyping.cmi | 0m00.35s | 84076 ko || +0m00.14s || 1284 ko | +40.00% | +1.52%
0m00.45s | 502992 ko | MCUtils.vo | 0m00.29s | 502540 ko || +0m00.16s || 452 ko | +55.17% | +0.08%
0m00.45s | 424300 ko | Transform.vo | 0m00.42s | 424744 ko || +0m00.03s || -444 ko | +7.14% | -0.10%
0m00.44s | 72656 ko | wGraph.cmx | 0m00.44s | 72664 ko || +0m00.00s || -8 ko | +0.00% | -0.01%
0m00.42s | 81004 ko | pCUICSafeChecker.cmx | 0m00.46s | 81072 ko || -0m00.04s || -68 ko | -8.69% | -0.08%
0m00.41s | 87512 ko | uGraph0.cmx | 0m00.39s | 88180 ko || +0m00.01s || -668 ko | +5.12% | -0.75%
0m00.40s | 433392 ko | MCPred.vo | 0m00.35s | 434140 ko || +0m00.05s || -748 ko | +14.28% | -0.17%
0m00.40s | 489404 ko | bytestring.vo | 0m00.42s | 488088 ko || -0m00.01s || 1316 ko | -4.76% | +0.26%
0m00.40s | 494060 ko | utils.vo | 0m00.34s | 492788 ko || +0m00.06s || 1272 ko | +17.64% | +0.25%
0m00.38s | 78976 ko | gen-src/universes0.cmx | 0m00.35s | 78828 ko || +0m00.03s || 148 ko | +8.57% | +0.18%
0m00.37s | 434100 ko | MCOption.vo | 0m00.42s | 433376 ko || -0m00.04s || 724 ko | -11.90% | +0.16%
0m00.37s | 60652 ko | gen-src/ast0.cmx | 0m00.28s | 59524 ko || +0m00.08s || 1128 ko | +32.14% | +1.89%
0m00.36s | 79136 ko | pCUICSafeConversion.cmx | 0m00.36s | 78428 ko || +0m00.00s || 708 ko | +0.00% | +0.90%
0m00.35s | 51680 ko | gen-src/environment.cmx | 0m00.24s | 51596 ko || +0m00.10s || 84 ko | +45.83% | +0.16%
0m00.35s | 78552 ko | gen-src/kernames.cmi | 0m00.29s | 78504 ko || +0m00.06s || 48 ko | +20.68% | +0.06%
0m00.35s | 42604 ko | gen-src/termEquality.cmx | 0m00.25s | 42784 ko || +0m00.09s || -180 ko | +39.99% | -0.42%
0m00.33s | 387988 ko | canonicaltries/String2pos.vo | 0m00.25s | 384984 ko || +0m00.08s || 3004 ko | +32.00% | +0.78%
0m00.33s | 60784 ko | gen-src/mCFSets.cmi | 0m00.23s | 60664 ko || +0m00.10s || 120 ko | +43.47% …- Loading branch information
1 parent
f0d3dda
commit 9c913d0