From 91712d3467c99c68e029d3562adc84581ed3c286 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 9 Apr 2023 17:45:23 -0700 Subject: [PATCH] Optimize `tmBind` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #441
Timing Diff

``` 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% | +0.19% 0m00.33s | 65564 ko | gen-src/mCFSets.cmx | 0m00.22s | 67676 ko || +0m00.11s || -2112 ko | +50.00% | -3.12% 0m00.32s | 433836 ko | Primitive.vo | 0m00.33s | 434512 ko || -0m00.01s || -676 ko | -3.03% | -0.15% 0m00.31s | 365888 ko | MCCompare.vo | 0m00.26s | 365684 ko || +0m00.04s || 204 ko | +19.23% | +0.05% 0m00.31s | 81440 ko | templateToPCUIC.cmx | 0m00.30s | 81432 ko || +0m00.01s || 8 ko | +3.33% | +0.00% 0m00.30s | 415464 ko | MCString.vo | 0m00.24s | 413968 ko || +0m00.06s || 1496 ko | +25.00% | +0.36% 0m00.30s | 367288 ko | ReflectEq.vo | 0m00.24s | 367688 ko || +0m00.06s || -400 ko | +25.00% | -0.10% 0m00.29s | 420536 ko | MCPrelude.vo | 0m00.37s | 418804 ko || -0m00.08s || 1732 ko | -21.62% | +0.41% 0m00.29s | 69972 ko | pCUICTypeChecker.cmx | 0m00.29s | 70564 ko || +0m00.00s || -592 ko | +0.00% | -0.83% 0m00.28s | 34904 ko | constr_quoter.cmx | 0m00.24s | 35004 ko || +0m00.04s || -100 ko | +16.66% | -0.28% 0m00.27s | 350580 ko | MCArith.vo | 0m00.27s | 351412 ko || +0m00.00s || -832 ko | +0.00% | -0.23% 0m00.25s | 306252 ko | MC_ExtrOCamlZPosInt.vo | 0m00.20s | 300928 ko || +0m00.04s || 5324 ko | +24.99% | +1.76% 0m00.25s | 356136 ko | Typed/ResultMonad.vo | 0m00.24s | 356724 ko || +0m00.01s || -588 ko | +4.16% | -0.16% 0m00.25s | 64280 ko | pCUICAst.cmx | 0m00.32s | 64164 ko || -0m00.07s || 116 ko | -21.87% | +0.18% 0m00.25s | 64204 ko | pCUICErrors.cmx | 0m00.29s | 65244 ko || -0m00.03s || -1040 ko | -13.79% | -1.59% 0m00.25s | 36516 ko | run_template_monad.cmx | 0m00.26s | 36392 ko || -0m00.01s || 124 ko | -3.84% | +0.34% 0m00.24s | 61968 ko | pCUICPretty.cmx | 0m00.22s | 63436 ko || +0m00.01s || -1468 ko | +9.09% | -2.31% 0m00.23s | 302968 ko | LibHypsNaming.vo | 0m00.19s | 302668 ko || +0m00.04s || 300 ko | +21.05% | +0.09% 0m00.23s | 54284 ko | uGraph0.cmi | 0m00.20s | 54508 ko || +0m00.03s || -224 ko | +15.00% | -0.41% 0m00.21s | 325860 ko | MCReflect.vo | 0m00.22s | 322344 ko || -0m00.01s || 3516 ko | -4.54% | +1.09% 0m00.21s | 59164 ko | gen-src/typing0.cmi | 0m00.17s | 59400 ko || +0m00.03s || -236 ko | +23.52% | -0.39% 0m00.20s | 56936 ko | pCUICAstUtils.cmx | 0m00.21s | 56204 ko || -0m00.00s || 732 ko | -4.76% | +1.30% 0m00.19s | 230068 ko | ByteCompare.vo | 0m00.12s | 228680 ko || +0m00.07s || 1388 ko | +58.33% | +0.60% 0m00.19s | 54372 ko | gen-src/mCMSets.cmx | 0m00.14s | 55836 ko || +0m00.04s || -1464 ko | +35.71% | -2.62% 0m00.19s | 33460 ko | gen-src/pretty.cmx | 0m00.15s | 33460 ko || +0m00.04s || 0 ko | +26.66% | +0.00% 0m00.19s | 63168 ko | gen-src/universes0.cmi | 0m00.20s | 63312 ko || -0m00.01s || -144 ko | -5.00% | -0.22% 0m00.19s | 56212 ko | pCUICCases.cmx | 0m00.19s | 56580 ko || +0m00.00s || -368 ko | +0.00% | -0.65% 0m00.19s | 61816 ko | pCUICEqualityDec.cmx | 0m00.16s | 60000 ko || +0m00.03s || 1816 ko | +18.75% | +3.02% 0m00.18s | 42944 ko | gen-src/fMapList.cmx | 0m00.14s | 42944 ko || +0m00.03s || 0 ko | +28.57% | +0.00% 0m00.18s | 60576 ko | pCUICWfEnvImpl.cmx | 0m00.16s | 61128 ko || +0m00.01s || -552 ko | +12.49% | -0.90% 0m00.18s | 53500 ko | wGraph.cmi | 0m00.13s | 52192 ko || +0m00.04s || 1308 ko | +38.46% | +2.50% 0m00.17s | 269492 ko | MC_ExtrOCamlInt63.vo | 0m00.20s | 268896 ko || -0m00.03s || 596 ko | -15.00% | +0.22% 0m00.17s | 34600 ko | constr_denoter.cmx | 0m00.21s | 33128 ko || -0m00.03s || 1472 ko | -19.04% | +4.44% 0m00.17s | 60416 ko | g_metacoq_safechecker.cmx | 0m00.16s | 60576 ko || +0m00.01s || -160 ko | +6.25% | -0.26% 0m00.17s | 40616 ko | gen-src/ast_denoter.cmx | 0m00.14s | 40740 ko || +0m00.03s || -124 ko | +21.42% | -0.30% 0m00.17s | 33196 ko | gen-src/quoter.cmx | 0m00.17s | 33256 ko || +0m00.00s || -60 ko | +0.00% | -0.18% 0m00.17s | 57656 ko | pCUICSafeReduce.cmx | 0m00.18s | 59056 ko || -0m00.00s || -1400 ko | -5.55% | -2.37% 0m00.17s | 32452 ko | quoter.cmx | 0m00.18s | 32596 ko || -0m00.00s || -144 ko | -5.55% | -0.44% 0m00.16s | 22292 ko | gen-src/binPos.cmx | 0m00.16s | 22164 ko || +0m00.00s || 128 ko | +0.00% | +0.57% 0m00.16s | 48200 ko | gen-src/mCMSets.cmi | 0m00.13s | 50060 ko || +0m00.03s || -1860 ko | +23.07% | -3.71% 0m00.16s | 26772 ko | gen-src/mSetAVL.cmx | 0m00.12s | 26532 ko || +0m00.04s || 240 ko | +33.33% | +0.90% 0m00.16s | 55852 ko | pCUICReflect.cmx | 0m00.18s | 56808 ko || -0m00.01s || -956 ko | -11.11% | -1.68% 0m00.15s | 35664 ko | gen-src/ast_quoter.cmx | 0m00.11s | 35524 ko || +0m00.03s || 140 ko | +36.36% | +0.39% 0m00.15s | 32096 ko | gen-src/induction.cmx | 0m00.12s | 31944 ko || +0m00.03s || 152 ko | +25.00% | +0.47% 0m00.15s | 23228 ko | metacoq_safechecker_plugin.cmxs | 0m00.18s | 23244 ko || -0m00.03s || -16 ko | -16.66% | -0.06% 0m00.15s | 55836 ko | pCUICProgram.cmx | 0m00.14s | 56296 ko || +0m00.00s || -460 ko | +7.14% | -0.81% 0m00.14s | 30400 ko | g_template_coq.cmx | 0m00.12s | 30304 ko || +0m00.02s || 96 ko | +16.66% | +0.31% 0m00.14s | 31084 ko | gen-src/astUtils.cmx | 0m00.14s | 31184 ko || +0m00.00s || -100 ko | +0.00% | -0.32% 0m00.14s | 21968 ko | gen-src/hexadecimal.cmx | 0m00.07s | 21944 ko || +0m00.07s || 24 ko | +100.00% | +0.10% 0m00.14s | 21452 ko | gen-src/peanoNat.cmx | 0m00.10s | 21592 ko || +0m00.04s || -140 ko | +40.00% | -0.64% 0m00.14s | 56696 ko | pCUICPosition.cmx | 0m00.17s | 55648 ko || -0m00.03s || 1048 ko | -17.64% | +1.88% 0m00.13s | 160368 ko | MCRelations.vo | 0m00.12s | 157160 ko || +0m00.01s || 3208 ko | +8.33% | +2.04% 0m00.13s | 27840 ko | gen-src/basicAst.cmx | 0m00.10s | 27876 ko || +0m00.03s || -36 ko | +30.00% | -0.12% 0m00.13s | 61280 ko | metacoq_safechecker_plugin.cmx | 0m00.15s | 62444 ko || -0m00.01s || -1164 ko | -13.33% | -1.86% 0m00.13s | 51800 ko | pCUICProgram.cmi | 0m00.09s | 52108 ko || +0m00.04s || -308 ko | +44.44% | -0.59% 0m00.12s | 22884 ko | gen-src/byteCompare.cmx | 0m00.07s | 22956 ko || +0m00.04s || -72 ko | +71.42% | -0.31% 0m00.12s | 34064 ko | gen-src/run_extractable.cmx | 0m00.11s | 33944 ko || +0m00.00s || 120 ko | +9.09% | +0.35% 0m00.12s | 51748 ko | pCUICAst.cmi | 0m00.14s | 51976 ko || -0m00.02s || -228 ko | -14.28% | -0.43% 0m00.12s | 56480 ko | pCUICTyping.cmx | 0m00.13s | 55268 ko || -0m00.01s || 1212 ko | -7.69% | +2.19% 0m00.11s | 31848 ko | gen-src/ast_quoter.cmo | 0m00.08s | 31804 ko || +0m00.03s || 44 ko | +37.50% | +0.13% 0m00.11s | 21416 ko | gen-src/binPosDef.cmx | 0m00.13s | 21636 ko || -0m00.02s || -220 ko | -15.38% | -1.01% 0m00.11s | 22140 ko | gen-src/mSetList.cmx | 0m00.08s | 22140 ko || +0m00.03s || 0 ko | +37.50% | +0.00% 0m00.11s | 30352 ko | gen-src/tm_util.cmx | 0m00.09s | 30184 ko || +0m00.02s || 168 ko | +22.22% | +0.55% 0m00.11s | 30404 ko | plugin_core.cmx | 0m00.10s | 30420 ko || +0m00.00s || -16 ko | +9.99% | -0.05% 0m00.10s | 22180 ko | gen-src/binInt.cmx | 0m00.10s | 22128 ko || +0m00.00s || 52 ko | +0.00% | +0.23% 0m00.10s | 30216 ko | gen-src/environment.cmi | 0m00.06s | 30240 ko || +0m00.04s || -24 ko | +66.66% | -0.07% 0m00.10s | 30900 ko | gen-src/plugin_core.cmx | 0m00.10s | 31064 ko || +0m00.00s || -164 ko | +0.00% | -0.52% 0m00.10s | 56064 ko | pCUICWfEnv.cmx | 0m00.13s | 56340 ko || -0m00.03s || -276 ko | -23.07% | -0.48% 0m00.10s | 52216 ko | pCUICWfEnvImpl.cmi | 0m00.08s | 52540 ko || +0m00.02s || -324 ko | +25.00% | -0.61% 0m00.09s | 24012 ko | constr_reification.cmx | 0m00.09s | 24188 ko || +0m00.00s || -176 ko | +0.00% | -0.72% 0m00.09s | 25580 ko | gen-src/fMapList.cmi | 0m00.08s | 25624 ko || +0m00.00s || -44 ko | +12.49% | -0.17% 0m00.09s | 20944 ko | gen-src/int0.cmx | 0m00.06s | 20892 ko || +0m00.03s || 52 ko | +50.00% | +0.24% 0m00.09s | 22088 ko | gen-src/mCList.cmx | 0m00.08s | 22068 ko || +0m00.00s || 20 ko | +12.49% | +0.09% 0m00.09s | 21212 ko | gen-src/specFloat.cmx | 0m00.05s | 21236 ko || +0m00.03s || -24 ko | +79.99% | -0.11% 0m00.09s | 52588 ko | pCUICSafeChecker.cmi | 0m00.09s | 52920 ko || +0m00.00s || -332 ko | +0.00% | -0.62% 0m00.09s | 25340 ko | template_monad.cmx | 0m00.11s | 25836 ko || -0m00.02s || -496 ko | -18.18% | -1.91% 0m00.09s | 30400 ko | tm_util.cmx | 0m00.10s | 30564 ko || -0m00.01s || -164 ko | -10.00% | -0.53% 0m00.08s | 68128 ko | ExtractableLoader.vo | 0m00.04s | 67532 ko || +0m00.04s || 596 ko | +100.00% | +0.88% 0m00.08s | 37104 ko | gen-src/ast0.cmi | 0m00.09s | 37008 ko || -0m00.00s || 96 ko | -11.11% | +0.25% 0m00.08s | 27304 ko | gen-src/quoter.cmo | 0m00.07s | 27188 ko || +0m00.00s || 116 ko | +14.28% | +0.42% 0m00.08s | 28244 ko | gen-src/reflect.cmx | 0m00.06s | 28300 ko || +0m00.02s || -56 ko | +33.33% | -0.19% 0m00.08s | 56428 ko | pCUICEquality.cmx | 0m00.09s | 55388 ko || -0m00.00s || 1040 ko | -11.11% | +1.87% 0m00.08s | 55032 ko | safeTemplateChecker.cmx | 0m00.07s | 55436 ko || +0m00.00s || -404 ko | +14.28% | -0.72% 0m00.07s | 112984 ko | MCProd.vo | 0m00.09s | 113088 ko || -0m00.01s || -104 ko | -22.22% | -0.09% 0m00.07s | 63888 ko | MCTactics/FindHyp.vo | 0m00.03s | 63900 ko || +0m00.04s || -12 ko | +133.33% | -0.01% 0m00.07s | 71888 ko | MCTactics/GeneralizeOverHoles.vo | 0m00.05s | 72364 ko || +0m00.02s || -476 ko | +40.00% | -0.65% 0m00.07s | 25744 ko | denoter.cmx | 0m00.10s | 25752 ko || -0m00.03s || -8 ko | -30.00% | -0.03% 0m00.07s | 20076 ko | gen-src/decimal.cmx | 0m00.06s | 20084 ko || +0m00.01s || -8 ko | +16.66% | -0.03% 0m00.07s | 27904 ko | gen-src/extractable.cmx | 0m00.06s | 27904 ko || +0m00.01s || 0 ko | +16.66% | +0.00% 0m00.07s | 21556 ko | gen-src/fMapFacts.cmx | 0m00.11s | 21624 ko || -0m00.03s || -68 ko | -36.36% | -0.31% 0m00.07s | 20248 ko | gen-src/list0.cmx | 0m00.04s | 20216 ko || +0m00.03s || 32 ko | +75.00% | +0.15% 0m00.07s | 22660 ko | gen-src/mSetInterface.cmx | 0m00.08s | 22688 ko || -0m00.00s || -28 ko | -12.49% | -0.12% 0m00.07s | 53036 ko | pCUICAstUtils.cmi | 0m00.05s | 53108 ko || +0m00.02s || -72 ko | +40.00% | -0.13% 0m00.07s | 56100 ko | pCUICPrimitive.cmx | 0m00.04s | 55888 ko || +0m00.03s || 212 ko | +75.00% | +0.37% 0m00.07s | 52924 ko | pCUICSafeConversion.cmi | 0m00.07s | 51832 ko || +0m00.00s || 1092 ko | +0.00% | +2.10% 0m00.07s | 53672 ko | pCUICTypeChecker.cmi | 0m00.07s | 53404 ko || +0m00.00s || 268 ko | +0.00% | +0.50% 0m00.06s | 64788 ko | MCTactics/UniquePose.vo | 0m00.05s | 63364 ko || +0m00.00s || 1424 ko | +19.99% | +2.24% 0m00.06s | 52156 ko | extraction.cmi | 0m00.04s | 52576 ko || +0m00.01s || -420 ko | +49.99% | -0.79% 0m00.06s | 23176 ko | gen-src/all_Forall.cmi | 0m00.06s | 23184 ko || +0m00.00s || -8 ko | +0.00% | -0.03% 0m00.06s | 21548 ko | gen-src/binNat.cmx | 0m00.07s | 21500 ko || -0m00.01s || 48 ko | -14.28% | +0.22% 0m00.06s | 20932 ko | gen-src/bytestring.cmx | 0m00.05s | 20680 ko || +0m00.00s || 252 ko | +19.99% | +1.21% 0m00.06s | 25464 ko | gen-src/denoter.cmx | 0m00.07s | 25604 ko || -0m00.01s || -140 ko | -14.28% | -0.54% 0m00.06s | 21792 ko | gen-src/monad_utils.cmx | 0m00.06s | 21804 ko || +0m00.00s || -12 ko | +0.00% | -0.05% 0m00.06s | 20496 ko | gen-src/nat0.cmx | 0m00.06s | 20540 ko || +0m00.00s || -44 ko | +0.00% | -0.21% 0m00.06s | 26948 ko | gen-src/templateEnvMap.cmx | 0m00.05s | 27100 ko || +0m00.00s || -152 ko | +19.99% | -0.56% 0m00.06s | 55676 ko | pCUICNormal.cmx | 0m00.04s | 54744 ko || +0m00.01s || 932 ko | +49.99% | +1.70% 0m00.06s | 52936 ko | pCUICPosition.cmi | 0m00.05s | 52160 ko || +0m00.00s || 776 ko | +19.99% | +1.48% 0m00.06s | 52580 ko | pCUICPretty.cmi | 0m00.03s | 52356 ko || +0m00.03s || 224 ko | +100.00% | +0.42% 0m00.05s | 64436 ko | MCEquality.vo | 0m00.04s | 64024 ko || +0m00.01s || 412 ko | +25.00% | +0.64% 0m00.05s | 64152 ko | MCTactics/SpecializeBy.vo | 0m00.03s | 64468 ko || +0m00.02s || -316 ko | +66.66% | -0.49% 0m00.05s | 63544 ko | MCTactics/SplitInContext.vo | 0m00.06s | 63764 ko || -0m00.00s || -220 ko | -16.66% | -0.34% 0m00.05s | 64324 ko | MCTactics/Zeta1.vo | 0m00.04s | 63120 ko || +0m00.01s || 1204 ko | +25.00% | +1.90% 0m00.05s | 64756 ko | ToTemplate/Common/Transform.vo | 0m00.01s | 63028 ko || +0m00.04s || 1728 ko | +400.00% | +2.74% 0m00.05s | 63972 ko | ToTemplate/Utils/LibHypsNaming.vo | 0m00.06s | 64260 ko || -0m00.00s || -288 ko | -16.66% | -0.44% 0m00.05s | 64688 ko | ToTemplate/Utils/MCCompare.vo | 0m00.04s | 63780 ko || +0m00.01s || 908 ko | +25.00% | +1.42% 0m00.05s | 64648 ko | ToTemplate/Utils/MCEquality.vo | 0m00.04s | 62848 ko || +0m00.01s || 1800 ko | +25.00% | +2.86% 0m00.05s | 63184 ko | ToTemplate/Utils/MCPrelude.vo | 0m00.03s | 63244 ko || +0m00.02s || -60 ko | +66.66% | -0.09% 0m00.05s | 63444 ko | ToTemplate/Utils/monad_utils.vo | 0m00.03s | 63928 ko || +0m00.02s || -484 ko | +66.66% | -0.75% 0m00.05s | 20308 ko | gen-src/caml_byte.cmx | 0m00.02s | 20264 ko || +0m00.03s || 44 ko | +150.00% | +0.21% 0m00.05s | 24956 ko | gen-src/common0.cmx | 0m00.01s | 24968 ko || +0m00.04s || -12 ko | +400.00% | -0.04% 0m00.05s | 21600 ko | gen-src/mSetAVL.cmi | 0m00.04s | 21472 ko || +0m00.01s || 128 ko | +25.00% | +0.59% 0m00.05s | 21640 ko | gen-src/mSetProperties.cmx | 0m00.04s | 21748 ko || +0m00.01s || -108 ko | +25.00% | -0.49% 0m00.05s | 52024 ko | pCUICEqualityDec.cmi | 0m00.07s | 53116 ko || -0m00.02s || -1092 ko | -28.57% | -2.05% 0m00.05s | 53544 ko | pCUICPrimitive.cmi | 0m00.05s | 51996 ko || +0m00.00s || 1548 ko | +0.00% | +2.97% 0m00.05s | 53356 ko | pCUICReflect.cmi | 0m00.04s | 52920 ko || +0m00.01s || 436 ko | +25.00% | +0.82% 0m00.05s | 52840 ko | pCUICSafeReduce.cmi | 0m00.04s | 53716 ko || +0m00.01s || -876 ko | +25.00% | -1.63% 0m00.05s | 52440 ko | pCUICWfEnv.cmi | 0m00.04s | 51900 ko || +0m00.01s || 540 ko | +25.00% | +1.04% 0m00.05s | 52436 ko | safeTemplateChecker.cmi | 0m00.05s | 52184 ko || +0m00.00s || 252 ko | +0.00% | +0.48% 0m00.05s | 53192 ko | templateToPCUIC.cmi | 0m00.03s | 52180 ko || +0m00.02s || 1012 ko | +66.66% | +1.93% 0m00.05s | 25116 ko | template_coq.cmx | 0m00.05s | 25104 ko || +0m00.00s || 12 ko | +0.00% | +0.04% 0m00.05s | 17492 ko | template_coq.cmxs | 0m00.06s | 17264 ko || -0m00.00s || 228 ko | -16.66% | +1.32% 0m00.04s | 64396 ko | MCSquash.vo | 0m00.03s | 65120 ko || +0m00.01s || -724 ko | +33.33% | -1.11% 0m00.04s | 75012 ko | MCTactics/InHypUnderBindersDo.vo | 0m00.03s | 75244 ko || +0m00.01s || -232 ko | +33.33% | -0.30% 0m00.04s | 75048 ko | MCTactics/SpecializeUnderBindersBy.vo | 0m00.03s | 75612 ko || +0m00.01s || -564 ko | +33.33% | -0.74% 0m00.04s | 64320 ko | ToTemplate/Template/UnivSubst.vo | 0m00.03s | 63852 ko || +0m00.01s || 468 ko | +33.33% | +0.73% 0m00.04s | 64332 ko | ToTemplate/Utils/ByteCompareSpec.vo | 0m00.05s | 65008 ko || -0m00.01s || -676 ko | -20.00% | -1.03% 0m00.04s | 63356 ko | ToTemplate/Utils/ByteCompare_opt.vo | 0m00.02s | 63848 ko || +0m00.02s || -492 ko | +100.00% | -0.77% 0m00.04s | 62976 ko | ToTemplate/Utils/MCRelations.vo | 0m00.02s | 62948 ko || +0m00.02s || 28 ko | +100.00% | +0.04% 0m00.04s | 63604 ko | ToTemplate/Utils/MCString.vo | 0m00.05s | 64676 ko || -0m00.01s || -1072 ko | -20.00% | -1.65% 0m00.04s | 55940 ko | extraction.cmx | 0m00.06s | 56184 ko || -0m00.01s || -244 ko | -33.33% | -0.43% 0m00.04s | 19032 ko | gen-src/ascii.cmx | 0m00.02s | 18824 ko || +0m00.02s || 208 ko | +100.00% | +1.10% 0m00.04s | 23944 ko | gen-src/astUtils.cmi | 0m00.01s | 23852 ko || +0m00.03s || 92 ko | +300.00% | +0.38% 0m00.04s | 20280 ko | gen-src/cRelationClasses.cmx | 0m00.03s | 20256 ko || +0m00.01s || 24 ko | +33.33% | +0.11% 0m00.04s | 17972 ko | gen-src/datatypes.cmx | 0m00.02s | 18016 ko || +0m00.02s || -44 ko | +100.00% | -0.24% 0m00.04s | 18128 ko | gen-src/decimalString.cmx | 0m00.03s | 18068 ko || +0m00.01s || 60 ko | +33.33% | +0.33% 0m00.04s | 17836 ko | gen-src/equalities.cmx | 0m00.02s | 17760 ko || +0m00.02s || 76 ko | +100.00% | +0.42% 0m00.04s | 22764 ko | gen-src/induction.cmi | 0m00.03s | 22608 ko || +0m00.01s || 156 ko | +33.33% | +0.69% 0m00.04s | 18520 ko | gen-src/liftSubst.cmx | 0m00.01s | 18540 ko || +0m00.03s || -20 ko | +300.00% | -0.10% 0m00.04s | 18848 ko | gen-src/mCRelations.cmx | 0m00.03s | 18820 ko || +0m00.01s || 28 ko | +33.33% | +0.14% 0m00.04s | 56768 ko | gen-src/metacoq_template_plugin.cmxa | 0m00.03s | 56424 ko || +0m00.01s || 344 ko | +33.33% | +0.60% 0m00.04s | 14284 ko | gen-src/number.cmi | 0m00.02s | 14148 ko || +0m00.02s || 136 ko | +100.00% | +0.96% 0m00.04s | 18488 ko | gen-src/plugin_core.cmi | 0m00.03s | 18700 ko || +0m00.01s || -212 ko | +33.33% | -1.13% 0m00.04s | 20908 ko | gen-src/relation.cmx | 0m00.05s | 20868 ko || -0m00.01s || 40 ko | -20.00% | +0.19% 0m00.04s | 20120 ko | gen-src/specif.cmx | 0m00.04s | 20060 ko || +0m00.00s || 60 ko | +0.00% | +0.29% 0m00.04s | 53724 ko | pCUICErrors.cmi | 0m00.07s | 52756 ko || -0m00.03s || 968 ko | -42.85% | +1.83% 0m00.04s | 52452 ko | pCUICTyping.cmi | 0m00.06s | 52624 ko || -0m00.01s || -172 ko | -33.33% | -0.32% 0m00.04s | 52340 ko | ssrbool.cmi | 0m00.01s | 53336 ko || +0m00.03s || -996 ko | +300.00% | -1.86% 0m00.04s | 56588 ko | ssrbool.cmx | 0m00.04s | 55340 ko || +0m00.00s || 1248 ko | +0.00% | +2.25% 0m00.04s | 54624 ko | template_coq.cmxa | 0m00.13s | 54524 ko || -0m00.09s || 100 ko | -69.23% | +0.18% 0m00.03s | 71364 ko | Loader.vo | 0m00.05s | 70264 ko || -0m00.02s || 1100 ko | -40.00% | +1.56% 0m00.03s | 69916 ko | MCTactics/DestructHead.vo | 0m00.05s | 70224 ko || -0m00.02s || -308 ko | -40.00% | -0.43% 0m00.03s | 64720 ko | MCTactics/DestructHyps.vo | 0m00.04s | 64564 ko || -0m00.01s || 156 ko | -25.00% | +0.24% 0m00.03s | 64268 ko | MCTactics/Head.vo | 0m00.04s | 63564 ko || -0m00.01s || 704 ko | -25.00% | +1.10% 0m00.03s | 63672 ko | MCTactics/SpecializeAllWays.vo | 0m00.02s | 62968 ko || +0m00.00s || 704 ko | +49.99% | +1.11% 0m00.03s | 63312 ko | ToTemplate/Template/ReflectAst.vo | 0m00.02s | 64704 ko || +0m00.00s || -1392 ko | +49.99% | -2.15% 0m00.03s | 63156 ko | ToTemplate/Utils/MCPred.vo | 0m00.03s | 63308 ko || +0m00.00s || -152 ko | +0.00% | -0.24% 0m00.03s | 63536 ko | ToTemplate/Utils/MCSquash.vo | 0m00.03s | 64372 ko || +0m00.00s || -836 ko | +0.00% | -1.29% 0m00.03s | 24108 ko | gen-src/basicAst.cmi | 0m00.02s | 23584 ko || +0m00.00s || 524 ko | +49.99% | +2.22% 0m00.03s | 15708 ko | gen-src/binPos.cmi | 0m00.03s | 15776 ko || +0m00.00s || -68 ko | +0.00% | -0.43% 0m00.03s | 15036 ko | gen-src/binPosDef.cmi | 0m00.03s | 15236 ko || +0m00.00s || -200 ko | +0.00% | -1.31% 0m00.03s | 15152 ko | gen-src/cRelationClasses.cmi | 0m00.00s | 14964 ko || +0m00.03s || 188 ko | ∞ | +1.25% 0m00.03s | 18256 ko | gen-src/caml_bytestring.cmx | 0m00.02s | 18072 ko || +0m00.00s || 184 ko | +49.99% | +1.01% 0m00.03s | 16772 ko | gen-src/caml_nat.cmx | 0m00.01s | 16812 ko || +0m00.01s || -40 ko | +199.99% | -0.23% 0m00.03s | 17484 ko | gen-src/classes0.cmx | 0m00.01s | 17644 ko || +0m00.01s || -160 ko | +199.99% | -0.90% 0m00.03s | 21604 ko | gen-src/common0.cmi | 0m00.02s | 21580 ko || +0m00.00s || 24 ko | +49.99% | +0.11% 0m00.03s | 17500 ko | gen-src/compare_dec.cmx | 0m00.02s | 17532 ko || +0m00.00s || -32 ko | +49.99% | -0.18% 0m00.03s | 17440 ko | gen-src/config0.cmx | 0m00.02s | 17220 ko || +0m00.00s || 220 ko | +49.99% | +1.27% 0m00.03s | 14304 ko | gen-src/datatypes.cmi | 0m00.02s | 14408 ko || +0m00.00s || -104 ko | +49.99% | -0.72% 0m00.03s | 17160 ko | gen-src/eqDec.cmx | 0m00.00s | 17252 ko || +0m00.03s || -92 ko | ∞ | -0.53% 0m00.03s | 15052 ko | gen-src/fMapInterface.cmi | 0m00.02s | 15164 ko || +0m00.00s || -112 ko | +49.99% | -0.73% 0m00.03s | 17804 ko | gen-src/fMapInterface.cmx | 0m00.01s | 17668 ko || +0m00.01s || 136 ko | +199.99% | +0.76% 0m00.03s | 14784 ko | gen-src/floatOps.cmi | 0m00.00s | 14668 ko || +0m00.03s || 116 ko | ∞ | +0.79% 0m00.03s | 18136 ko | gen-src/floatOps.cmx | 0m00.03s | 18336 ko || +0m00.00s || -200 ko | +0.00% | -1.09% 0m00.03s | 14392 ko | gen-src/hexadecimal.cmi | 0m00.01s | 14208 ko || +0m00.01s || 184 ko | +199.99% | +1.29% 0m00.03s | 18508 ko | gen-src/hexadecimalString.cmx | 0m00.03s | 18464 ko || +0m00.00s || 44 ko | +0.00% | +0.23% 0m00.03s | 17404 ko | gen-src/logic1.cmx | 0m00.02s | 17372 ko || +0m00.00s || 32 ko | +49.99% | +0.18% 0m00.03s | 17664 ko | gen-src/logic2.cmx | 0m00.03s | 17744 ko || +0m00.00s || -80 ko | +0.00% | -0.45% 0m00.03s | 17792 ko | gen-src/mCCompare.cmx | 0m00.03s | 17952 ko || +0m00.00s || -160 ko | +0.00% | -0.89% 0m00.03s | 17832 ko | gen-src/mCList.cmi | 0m00.01s | 17960 ko || +0m00.01s || -128 ko | +199.99% | -0.71% 0m00.03s | 18260 ko | gen-src/mCOption.cmx | 0m00.02s | 18404 ko || +0m00.00s || -144 ko | +49.99% | -0.78% 0m00.03s | 17504 ko | gen-src/mCReflect.cmx | 0m00.03s | 17576 ko || +0m00.00s || -72 ko | +0.00% | -0.40% 0m00.03s | 18504 ko | gen-src/mCString.cmx | 0m00.02s | 18248 ko || +0m00.00s || 256 ko | +49.99% | +1.40% 0m00.03s | 14368 ko | gen-src/mCUtils.cmi | 0m00.02s | 14396 ko || +0m00.00s || -28 ko | +49.99% | -0.19% 0m00.03s | 17336 ko | gen-src/mCUtils.cmx | 0m00.01s | 17516 ko || +0m00.01s || -180 ko | +199.99% | -1.02% 0m00.03s | 18320 ko | gen-src/mSetDecide.cmx | 0m00.03s | 18144 ko || +0m00.00s || 176 ko | +0.00% | +0.97% 0m00.03s | 18452 ko | gen-src/mSetInterface.cmi | 0m00.03s | 18232 ko || +0m00.00s || 220 ko | +0.00% | +1.20% 0m00.03s | 18760 ko | gen-src/mSetList.cmi | 0m00.02s | 18692 ko || +0m00.00s || 68 ko | +49.99% | +0.36% 0m00.03s | 17600 ko | gen-src/number.cmx | 0m00.03s | 17612 ko || +0m00.00s || -12 ko | +0.00% | -0.06% 0m00.03s | 17680 ko | gen-src/orderedType0.cmx | 0m00.03s | 17816 ko || +0m00.00s || -136 ko | +0.00% | -0.76% 0m00.03s | 20348 ko | gen-src/orders.cmx | 0m00.02s | 20352 ko || +0m00.00s || -4 ko | +49.99% | -0.01% 0m00.03s | 14192 ko | gen-src/ordersAlt.cmi | 0m00.00s | 14416 ko || +0m00.03s || -224 ko | ∞ | -1.55% 0m00.03s | 17804 ko | gen-src/ordersAlt.cmx | 0m00.02s | 17752 ko || +0m00.00s || 52 ko | +49.99% | +0.29% 0m00.03s | 22192 ko | gen-src/reflect.cmi | 0m00.01s | 22152 ko || +0m00.01s || 40 ko | +199.99% | +0.18% 0m00.03s | 15152 ko | gen-src/specif.cmi | 0m00.02s | 15048 ko || +0m00.00s || 104 ko | +49.99% | +0.69% 0m00.03s | 20688 ko | gen-src/templateEnvMap.cmi | 0m00.02s | 19788 ko || +0m00.00s || 900 ko | +49.99% | +4.54% 0m00.03s | 21836 ko | gen-src/templateProgram.cmx | 0m00.03s | 21776 ko || +0m00.00s || 60 ko | +0.00% | +0.27% 0m00.03s | 26124 ko | gen-src/termEquality.cmi | 0m00.02s | 26284 ko || +0m00.00s || -160 ko | +49.99% | -0.60% 0m00.03s | 25568 ko | gen-src/tm_util.cmo | 0m00.05s | 26004 ko || -0m00.02s || -436 ko | -40.00% | -1.67% 0m00.03s | 20520 ko | gen-src/uint0.cmx | 0m00.06s | 20552 ko || -0m00.03s || -32 ko | -50.00% | -0.15% 0m00.03s | 17876 ko | gen-src/zArith_dec.cmx | 0m00.02s | 17944 ko || +0m00.00s || -68 ko | +49.99% | -0.37% 0m00.03s | 14592 ko | gen-src/zeven.cmi | 0m00.01s | 14340 ko || +0m00.01s || 252 ko | +199.99% | +1.75% 0m00.03s | 17632 ko | gen-src/zeven.cmx | 0m00.02s | 17584 ko || +0m00.00s || 48 ko | +49.99% | +0.27% 0m00.03s | 52588 ko | pCUICCases.cmi | 0m00.07s | 53160 ko || -0m00.04s || -572 ko | -57.14% | -1.07% 0m00.03s | 51968 ko | pCUICEquality.cmi | 0m00.05s | 53300 ko || -0m00.02s || -1332 ko | -40.00% | -2.49% 0m00.03s | 53396 ko | pCUICNormal.cmi | 0m00.03s | 53720 ko || +0m00.00s || -324 ko | +0.00% | -0.60% 0m00.02s | 63912 ko | ToTemplate/Common/Reflect.vo | 0m00.03s | 64164 ko || -0m00.00s || -252 ko | -33.33% | -0.39% 0m00.02s | 63936 ko | ToTemplate/Template/Induction.vo | 0m00.04s | 63844 ko || -0m00.02s || 92 ko | -50.00% | +0.14% 0m00.02s | 64032 ko | ToTemplate/Template/LiftSubst.vo | 0m00.03s | 63556 ko || -0m00.00s || 476 ko | -33.33% | +0.74% 0m00.02s | 14032 ko | gen-src/basics.cmi | 0m00.02s | 13908 ko || +0m00.00s || 124 ko | +0.00% | +0.89% 0m00.02s | 15296 ko | gen-src/binNat.cmi | 0m00.02s | 15560 ko || +0m00.00s || -264 ko | +0.00% | -1.69% 0m00.02s | 18188 ko | gen-src/byteCompareSpec.cmx | 0m00.03s | 18088 ko || -0m00.00s || 100 ko | -33.33% | +0.55% 0m00.02s | 15140 ko | gen-src/caml_bytestring.cmo | 0m00.02s | 15144 ko || +0m00.00s || -4 ko | +0.00% | -0.02% 0m00.02s | 13996 ko | gen-src/caml_nat.cmi | 0m00.01s | 14188 ko || +0m00.01s || -192 ko | +100.00% | -1.35% 0m00.02s | 14504 ko | gen-src/classes0.cmi | 0m00.00s | 14204 ko || +0m00.02s || 300 ko | ∞ | +2.11% 0m00.02s | 14072 ko | gen-src/compare_dec.cmi | 0m00.00s | 14340 ko || +0m00.02s || -268 ko | ∞ | -1.86% 0m00.02s | 14320 ko | gen-src/config0.cmi | 0m00.00s | 14148 ko || +0m00.02s || 172 ko | ∞ | +1.21% 0m00.02s | 17344 ko | gen-src/decidableType.cmx | 0m00.01s | 17024 ko || +0m00.01s || 320 ko | +100.00% | +1.87% 0m00.02s | 14432 ko | gen-src/decimal.cmi | 0m00.04s | 14224 ko || -0m00.02s || 208 ko | -50.00% | +1.46% 0m00.02s | 14616 ko | gen-src/decimalString.cmi | 0m00.01s | 14292 ko || +0m00.01s || 324 ko | +100.00% | +2.26% 0m00.02s | 19956 ko | gen-src/envMap.cmi | 0m00.02s | 19704 ko || +0m00.00s || 252 ko | +0.00% | +1.27% 0m00.02s | 22908 ko | gen-src/envMap.cmx | 0m00.01s | 23808 ko || +0m00.01s || -900 ko | +100.00% | -3.78% 0m00.02s | 14516 ko | gen-src/eqDecInstances.cmi | 0m00.00s | 14364 ko || +0m00.02s || 152 ko | ∞ | +1.05% 0m00.02s | 17856 ko | gen-src/eqDecInstances.cmx | 0m00.01s | 17800 ko || +0m00.01s || 56 ko | +100.00% | +0.31% 0m00.02s | 21468 ko | gen-src/extractable.cmi | 0m00.01s | 20192 ko || +0m00.01s || 1276 ko | +100.00% | +6.31% 0m00.02s | 15052 ko | gen-src/list0.cmi | 0m00.03s | 15032 ko || -0m00.00s || 20 ko | -33.33% | +0.13% 0m00.02s | 14760 ko | gen-src/logic0.cmi | 0m00.00s | 14744 ko || +0m00.02s || 16 ko | ∞ | +0.10% 0m00.02s | 17780 ko | gen-src/logic0.cmx | 0m00.01s | 17764 ko || +0m00.01s || 16 ko | +100.00% | +0.09% 0m00.02s | 14872 ko | gen-src/mCCompare.cmi | 0m00.02s | 14956 ko || +0m00.00s || -84 ko | +0.00% | -0.56% 0m00.02s | 14956 ko | gen-src/mCOption.cmi | 0m00.00s | 15032 ko || +0m00.02s || -76 ko | ∞ | -0.50% 0m00.02s | 14232 ko | gen-src/mCPrelude.cmi | 0m00.02s | 14256 ko || +0m00.00s || -24 ko | +0.00% | -0.16% 0m00.02s | 17524 ko | gen-src/mCPrelude.cmx | 0m00.01s | 17500 ko || +0m00.01s || 24 ko | +100.00% | +0.13% 0m00.02s | 17728 ko | gen-src/mCProd.cmx | 0m00.03s | 17628 ko || -0m00.00s || 100 ko | -33.33% | +0.56% 0m00.02s | 14604 ko | gen-src/mCReflect.cmi | 0m00.01s | 14452 ko || +0m00.01s || 152 ko | +100.00% | +1.05% 0m00.02s | 15128 ko | gen-src/mCRelations.cmi | 0m00.02s | 15184 ko || +0m00.00s || -56 ko | +0.00% | -0.36% 0m00.02s | 15096 ko | gen-src/mCString.cmi | 0m00.01s | 14972 ko || +0m00.01s || 124 ko | +100.00% | +0.82% 0m00.02s | 15200 ko | gen-src/mSetDecide.cmi | 0m00.02s | 14992 ko || +0m00.00s || 208 ko | +0.00% | +1.38% 0m00.02s | 18032 ko | gen-src/mSetFacts.cmx | 0m00.03s | 18084 ko || -0m00.00s || -52 ko | -33.33% | -0.28% 0m00.02s | 18584 ko | gen-src/mSetProperties.cmi | 0m00.02s | 18552 ko || +0m00.00s || 32 ko | +0.00% | +0.17% 0m00.02s | 17856 ko | gen-src/ordersFacts.cmx | 0m00.03s | 17836 ko || -0m00.00s || 20 ko | -33.33% | +0.11% 0m00.02s | 13976 ko | gen-src/ordersLists.cmi | 0m00.00s | 13952 ko || +0m00.02s || 24 ko | ∞ | +0.17% 0m00.02s | 14452 ko | gen-src/ordersTac.cmi | 0m00.01s | 14400 ko || +0m00.01s || 52 ko | +100.00% | +0.36% 0m00.02s | 17700 ko | gen-src/ordersTac.cmx | 0m00.02s | 17500 ko || +0m00.00s || 200 ko | +0.00% | +1.14% 0m00.02s | 15432 ko | gen-src/peanoNat.cmi | 0m00.01s | 15388 ko || +0m00.01s || 44 ko | +100.00% | +0.28% 0m00.02s | 14488 ko | gen-src/primInt63.cmi | 0m00.00s | 14324 ko || +0m00.02s || 164 ko | ∞ | +1.14% 0m00.02s | 17676 ko | gen-src/primInt63.cmx | 0m00.01s | 17604 ko || +0m00.01s || 72 ko | +100.00% | +0.40% 0m00.02s | 19092 ko | gen-src/primitive.cmx | 0m00.01s | 19096 ko || +0m00.01s || -4 ko | +100.00% | -0.02% 0m00.02s | 18632 ko | gen-src/string0.cmx | 0m00.03s | 18748 ko || -0m00.00s || -116 ko | -33.33% | -0.61% 0m00.02s | 14364 ko | gen-src/sumbool.cmi | 0m00.02s | 14328 ko || +0m00.00s || 36 ko | +0.00% | +0.25% 0m00.02s | 17372 ko | gen-src/sumbool.cmx | 0m00.01s | 17368 ko || +0m00.01s || 4 ko | +100.00% | +0.02% 0m00.02s | 17828 ko | gen-src/templateProgram.cmi | 0m00.03s | 18220 ko || -0m00.00s || -392 ko | -33.33% | -2.15% 0m00.02s | 14712 ko | gen-src/transform.cmi | 0m00.01s | 15056 ko || +0m00.01s || -344 ko | +100.00% | -2.28% 0m00.02s | 18084 ko | gen-src/transform.cmx | 0m00.03s | 18292 ko || -0m00.00s || -208 ko | -33.33% | -1.13% 0m00.02s | 15340 ko | gen-src/uint0.cmi | 0m00.00s | 15244 ko || +0m00.02s || 96 ko | ∞ | +0.62% 0m00.02s | 14720 ko | gen-src/zbool.cmi | 0m00.01s | 14372 ko || +0m00.01s || 348 ko | +100.00% | +2.42% 0m00.02s | 17468 ko | gen-src/zbool.cmx | 0m00.02s | 17580 ko || +0m00.00s || -112 ko | +0.00% | -0.63% 0m00.02s | 18476 ko | gen-src/zpower.cmx | 0m00.02s | 18416 ko || +0m00.00s || 60 ko | +0.00% | +0.32% 0m00.02s | 18260 ko | plugin_core.cmi | 0m00.02s | 17984 ko || +0m00.00s || 276 ko | +0.00% | +1.53% 0m00.02s | 14764 ko | run_template_monad.cmi | 0m00.02s | 14876 ko || +0m00.00s || -112 ko | +0.00% | -0.75% 0m00.02s | 16640 ko | template_monad.cmi | 0m00.03s | 16688 ko || -0m00.00s || -48 ko | -33.33% | -0.28% 0m00.01s | 64840 ko | ToTemplate/Utils/ByteCompare.vo | 0m00.05s | 63404 ko || -0m00.04s || 1436 ko | -80.00% | +2.26% 0m00.01s | 14732 ko | gen-src/ascii.cmi | 0m00.01s | 14760 ko || +0m00.00s || -28 ko | +0.00% | -0.18% 0m00.01s | 14148 ko | gen-src/binNums.cmi | 0m00.01s | 14232 ko || +0m00.00s || -84 ko | +0.00% | -0.59% 0m00.01s | 17324 ko | gen-src/binNums.cmx | 0m00.02s | 17444 ko || -0m00.01s || -120 ko | -50.00% | -0.68% 0m00.01s | 14204 ko | gen-src/bool.cmi | 0m00.02s | 14220 ko || -0m00.01s || -16 ko | -50.00% | -0.11% 0m00.01s | 17556 ko | gen-src/bool.cmx | 0m00.01s | 17476 ko || +0m00.00s || 80 ko | +0.00% | +0.45% 0m00.01s | 14280 ko | gen-src/byte0.cmi | 0m00.00s | 14364 ko || +0m00.01s || -84 ko | ∞ | -0.58% 0m00.01s | 15692 ko | gen-src/byteCompare.cmi | 0m00.00s | 15624 ko || +0m00.01s || 68 ko | ∞ | +0.43% 0m00.01s | 13868 ko | gen-src/decidableType.cmi | 0m00.00s | 13844 ko || +0m00.01s || 24 ko | ∞ | +0.17% 0m00.01s | 14872 ko | gen-src/equalities.cmi | 0m00.00s | 14828 ko || +0m00.01s || 44 ko | ∞ | +0.29% 0m00.01s | 18532 ko | gen-src/fMapFacts.cmi | 0m00.03s | 18524 ko || -0m00.01s || 8 ko | -66.66% | +0.04% 0m00.01s | 14152 ko | gen-src/hexadecimalString.cmi | 0m00.00s | 14188 ko || +0m00.01s || -36 ko | ∞ | -0.25% 0m00.01s | 15440 ko | gen-src/liftSubst.cmi | 0m00.01s | 15328 ko || +0m00.00s || 112 ko | +0.00% | +0.73% 0m00.01s | 14724 ko | gen-src/logic2.cmi | 0m00.00s | 14520 ko || +0m00.01s || 204 ko | ∞ | +1.40% 0m00.01s | 14864 ko | gen-src/mCProd.cmi | 0m00.01s | 14448 ko || +0m00.00s || 416 ko | +0.00% | +2.87% 0m00.01s | 15212 ko | gen-src/mSetFacts.cmi | 0m00.00s | 15148 ko || +0m00.01s || 64 ko | ∞ | +0.42% 0m00.01s | 14604 ko | gen-src/nat0.cmi | 0m00.01s | 14756 ko || +0m00.00s || -152 ko | +0.00% | -1.03% 0m00.01s | 14220 ko | gen-src/orderedType0.cmi | 0m00.01s | 14380 ko || +0m00.00s || -160 ko | +0.00% | -1.11% 0m00.01s | 17500 ko | gen-src/orderedTypeAlt.cmx | 0m00.01s | 17440 ko || +0m00.00s || 60 ko | +0.00% | +0.34% 0m00.01s | 17200 ko | gen-src/ordersLists.cmx | 0m00.03s | 17408 ko || -0m00.01s || -208 ko | -66.66% | -1.19% 0m00.01s | 22744 ko | gen-src/pretty.cmi | 0m00.03s | 22688 ko || -0m00.01s || 56 ko | -66.66% | +0.24% 0m00.01s | 15088 ko | gen-src/primitive.cmi | 0m00.00s | 15168 ko || +0m00.01s || -80 ko | ∞ | -0.52% 0m00.01s | 14596 ko | gen-src/reflectEq.cmi | 0m00.02s | 14512 ko || -0m00.01s || 84 ko | -50.00% | +0.57% 0m00.01s | 17936 ko | gen-src/reflectEq.cmx | 0m00.02s | 18068 ko || -0m00.01s || -132 ko | -50.00% | -0.73% 0m00.01s | 14592 ko | gen-src/reification.cmo | 0m00.00s | 14552 ko || +0m00.01s || 40 ko | ∞ | +0.27% 0m00.01s | 17460 ko | gen-src/reification.cmx | 0m00.01s | 17348 ko || +0m00.00s || 112 ko | +0.00% | +0.64% 0m00.01s | 17172 ko | gen-src/relation.cmi | 0m00.02s | 16968 ko || -0m00.01s || 204 ko | -50.00% | +1.20% 0m00.01s | 15436 ko | gen-src/run_extractable.cmi | 0m00.00s | 15576 ko || +0m00.01s || -140 ko | ∞ | -0.89% 0m00.01s | 14052 ko | gen-src/signature.cmi | 0m00.02s | 13820 ko || -0m00.01s || 232 ko | -50.00% | +1.67% 0m00.01s | 16976 ko | gen-src/signature.cmx | 0m00.01s | 16864 ko || +0m00.00s || 112 ko | +0.00% | +0.66% 0m00.01s | 15172 ko | gen-src/specFloat.cmi | 0m00.02s | 15088 ko || -0m00.01s || 84 ko | -50.00% | +0.55% 0m00.01s | 14580 ko | gen-src/string0.cmi | 0m00.00s | 14572 ko || +0m00.01s || 8 ko | ∞ | +0.05% 0m00.01s | 14892 ko | gen-src/zArith_dec.cmi | 0m00.02s | 14856 ko || -0m00.01s || 36 ko | -50.00% | +0.24% 0m00.01s | 14972 ko | gen-src/zpower.cmi | 0m00.00s | 14988 ko || +0m00.01s || -16 ko | ∞ | -0.10% 0m00.01s | 54776 ko | metacoq_safechecker_plugin.cmxa | 0m00.04s | 54728 ko || -0m00.03s || 48 ko | -75.00% | +0.08% 0m00.01s | 16944 ko | reification.cmx | 0m00.01s | 16792 ko || +0m00.00s || 152 ko | +0.00% | +0.90% 0m00.00s | 17088 ko | gen-src/basics.cmx | 0m00.01s | 17096 ko || -0m00.01s || -8 ko | -100.00% | -0.04% 0m00.00s | 15496 ko | gen-src/binInt.cmi | 0m00.03s | 15540 ko || -0m00.03s || -44 ko | -100.00% | -0.28% 0m00.00s | 15616 ko | gen-src/byte.cmi | 0m00.02s | 15256 ko || -0m00.02s || 360 ko | -100.00% | +2.35% 0m00.00s | 14560 ko | gen-src/byteCompareSpec.cmi | 0m00.01s | 14776 ko || -0m00.01s || -216 ko | -100.00% | -1.46% 0m00.00s | 15268 ko | gen-src/bytestring.cmi | 0m00.02s | 15340 ko || -0m00.02s || -72 ko | -100.00% | -0.46% 0m00.00s | 14092 ko | gen-src/caml_byte.cmi | 0m00.01s | 13968 ko || -0m00.01s || 124 ko | -100.00% | +0.88% 0m00.00s | 13968 ko | gen-src/eqDec.cmi | 0m00.01s | 13804 ko || -0m00.01s || 164 ko | -100.00% | +1.18% 0m00.00s | 15012 ko | gen-src/int0.cmi | 0m00.02s | 15164 ko || -0m00.02s || -152 ko | -100.00% | -1.00% 0m00.00s | 14228 ko | gen-src/logic1.cmi | 0m00.01s | 14100 ko || -0m00.01s || 128 ko | -100.00% | +0.90% 0m00.00s | 15884 ko | gen-src/monad_utils.cmi | 0m00.00s | 15892 ko || +0m00.00s || -8 ko | N/A | -0.05% 0m00.00s | 14212 ko | gen-src/orderedTypeAlt.cmi | 0m00.01s | 14164 ko || -0m00.01s || 48 ko | -100.00% | +0.33% 0m00.00s | 15188 ko | gen-src/orders.cmi | 0m00.02s | 15268 ko || -0m00.02s || -80 ko | -100.00% | -0.52% 0m00.00s | 14876 ko | gen-src/ordersFacts.cmi | 0m00.00s | 14592 ko || +0m00.00s || 284 ko | N/A | +1.94% 0m00.00s | 14612 ko | gen-src/primFloat.cmi | 0m00.02s | 14920 ko || -0m00.02s || -308 ko | -100.00% | -2.06% 0m00.00s | 17668 ko | gen-src/primFloat.cmx | 0m00.01s | 17776 ko || -0m00.01s || -108 ko | -100.00% | -0.60% ```

--- template-coq/theories/TemplateMonad/Core.v | 5 ++--- test-suite/bug441.v | 2 -- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/template-coq/theories/TemplateMonad/Core.v b/template-coq/theories/TemplateMonad/Core.v index f06d419a8..524076a35 100644 --- a/template-coq/theories/TemplateMonad/Core.v +++ b/template-coq/theories/TemplateMonad/Core.v @@ -97,9 +97,8 @@ Definition TemplateMonad_UnoptimizedMonad@{t u} : Monad@{t u} TemplateMonad@{t u Definition TemplateMonad_OptimizedMonad@{t u} : Monad@{t u} TemplateMonad@{t u} := {| ret := @tmReturn ; bind := @tmOptimizedBind |}. -(* We don't want to make the optimized monad an instance, because it blows up performance in some cases *) Definition TemplateMonad_Monad@{t u} : Monad@{t u} TemplateMonad@{t u} := - Eval hnf in TemplateMonad_UnoptimizedMonad. + Eval hnf in TemplateMonad_OptimizedMonad. Global Existing Instance TemplateMonad_Monad. Polymorphic Definition tmDefinitionRed @@ -202,7 +201,7 @@ Definition TypeInstanceOptimized : Common.TMInstance := |}. Definition TypeInstance : Common.TMInstance := - Eval hnf in TypeInstanceUnoptimized. + Eval hnf in TypeInstanceOptimized. Definition tmQuoteUniverse@{U t u} : TemplateMonad@{t u} Universe.t := u <- @tmQuote Prop (Type@{U} -> True);; diff --git a/test-suite/bug441.v b/test-suite/bug441.v index 623edbf37..27f86d922 100644 --- a/test-suite/bug441.v +++ b/test-suite/bug441.v @@ -1,8 +1,6 @@ From MetaCoq Require Import Template.All. Import MCMonadNotation. -#[local] Existing Instance TemplateMonad_OptimizedMonad. - Fixpoint tm_double n : TemplateMonad nat := match n with | 0 => ret 0