From f69c4ccb2208c75e8c5c93635f564ff792ab5202 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 6 Oct 2022 20:45:19 +0530 Subject: [PATCH] `Global Strategy -1000 [UnderLets.to_expr].` (#75) We will need this for using `UnderLets.to_expr` in reification
Timing Diff

``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 10m00.73s | 1401132 ko | Total Time / Peak Mem | 10m01.39s | 1401188 ko || -0m00.66s || -56 ko | -0.11% | -0.00% ------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 1m49.70s | 1142680 ko | Rewriter/Rewriter/Wf.vo | 1m50.19s | 1142852 ko || -0m00.48s || -172 ko | -0.44% | -0.01% 0m59.71s | 728232 ko | Rewriter/Language/UnderLetsProofs.vo | 0m59.61s | 727760 ko || +0m00.10s || 472 ko | +0.16% | +0.06% 0m54.69s | 1114640 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo | 0m54.64s | 1114536 ko || +0m00.04s || 104 ko | +0.09% | +0.00% 0m54.36s | 1401132 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo | 0m54.15s | 1401188 ko || +0m00.21s || -56 ko | +0.38% | -0.00% 0m53.42s | 1059016 ko | Rewriter/Rewriter/Examples.vo | 0m53.27s | 1058944 ko || +0m00.14s || 72 ko | +0.28% | +0.00% 0m52.22s | 941700 ko | Rewriter/Rewriter/InterpProofs.vo | 0m52.42s | 941852 ko || -0m00.20s || -152 ko | -0.38% | -0.01% 0m48.30s | 790584 ko | Rewriter/Rewriter/ProofsCommon.vo | 0m48.53s | 791528 ko || -0m00.23s || -944 ko | -0.47% | -0.11% 0m29.51s | 923852 ko | Rewriter/Rewriter/Examples/PrefixSums.vo | 0m29.65s | 923840 ko || -0m00.13s || 12 ko | -0.47% | +0.00% 0m26.67s | 679988 ko | Rewriter/Language/Wf.vo | 0m26.62s | 679904 ko || +0m00.05s || 84 ko | +0.18% | +0.01% 0m23.43s | 886412 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo | 0m23.44s | 886340 ko || -0m00.01s || 72 ko | -0.04% | +0.00% 0m17.70s | 574524 ko | Rewriter/Language/Inversion.vo | 0m17.71s | 574636 ko || -0m00.01s || -112 ko | -0.05% | -0.01% 0m15.87s | 734496 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo | 0m15.82s | 734664 ko || +0m00.04s || -168 ko | +0.31% | -0.02% 0m11.88s | 636892 ko | Rewriter/Demo.vo | 0m11.91s | 636984 ko || -0m00.02s || -92 ko | -0.25% | -0.01% 0m08.84s | 506792 ko | Rewriter/Language/IdentifiersLibraryProofs.vo | 0m08.73s | 506796 ko || +0m00.10s || -4 ko | +1.26% | -0.00% 0m05.90s | 455204 ko | Rewriter/Util/ListUtil.vo | 0m05.93s | 455216 ko || -0m00.02s || -12 ko | -0.50% | -0.00% 0m04.04s | 469224 ko | Rewriter/Language/IdentifiersBasicLibrary.vo | 0m04.05s | 469108 ko || -0m00.00s || 116 ko | -0.24% | +0.02% 0m02.42s | 423132 ko | Rewriter/Util/Bool/Reflect.vo | 0m02.48s | 423280 ko || -0m00.06s || -148 ko | -2.41% | -0.03% 0m01.47s | 409872 ko | Rewriter/Util/ListUtil/Forall.vo | 0m01.47s | 409924 ko || +0m00.00s || -52 ko | +0.00% | -0.01% 0m01.24s | 466968 ko | Rewriter/Language/IdentifiersLibrary.vo | 0m01.24s | 466960 ko || +0m00.00s || 8 ko | +0.00% | +0.00% 0m01.24s | 409320 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness.vo | 0m01.23s | 409188 ko || +0m00.01s || 132 ko | +0.81% | +0.03% 0m00.93s | 413512 ko | Rewriter/Util/NatUtil.vo | 0m00.93s | 413564 ko || +0m00.00s || -52 ko | +0.00% | -0.01% 0m00.91s | 465564 ko | Rewriter/Rewriter/Rewriter.vo | 0m00.99s | 465596 ko || -0m00.07s || -32 ko | -8.08% | -0.00% 0m00.90s | 475652 ko | Rewriter/Rewriter/Reify.vo | 0m00.92s | 475652 ko || -0m00.02s || 0 ko | -2.17% | +0.00% 0m00.85s | 444856 ko | Rewriter/Language/Language.vo | 0m00.86s | 444800 ko || -0m00.01s || 56 ko | -1.16% | +0.01% 0m00.74s | 488860 ko | Rewriter/Rewriter/AllTactics.vo | 0m00.82s | 488904 ko || -0m00.07s || -44 ko | -9.75% | -0.00% 0m00.73s | 408496 ko | Rewriter/Rewriter/Examples/PerfTesting/Sample.vo | 0m00.76s | 408600 ko || -0m00.03s || -104 ko | -3.94% | -0.02% 0m00.65s | 379960 ko | Rewriter/Util/Decidable.vo | 0m00.61s | 379904 ko || +0m00.04s || 56 ko | +6.55% | +0.01% 0m00.59s | 456852 ko | Rewriter/Language/IdentifiersGenerate.vo | 0m00.54s | 456948 ko || +0m00.04s || -96 ko | +9.25% | -0.02% 0m00.59s | 471464 ko | Rewriter/Rewriter/ProofsCommonTactics.vo | 0m00.61s | 471260 ko || -0m00.02s || 204 ko | -3.27% | +0.04% 0m00.57s | 480560 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo | 0m00.49s | 480300 ko || +0m00.07s || 260 ko | +16.32% | +0.05% 0m00.53s | 457920 ko | Rewriter/Language/IdentifiersGenerateProofs.vo | 0m00.47s | 457832 ko || +0m00.06s || 88 ko | +12.76% | +0.01% 0m00.53s | 479060 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo | 0m00.56s | 478932 ko || -0m00.03s || 128 ko | -5.35% | +0.02% 0m00.50s | 480536 ko | Rewriter/Util/plugins/RewriterBuild.vo | 0m00.45s | 480496 ko || +0m00.04s || 40 ko | +11.11% | +0.00% 0m00.49s | 441316 ko | Rewriter/Language/IdentifiersBasicGenerate.vo | 0m00.49s | 441204 ko || +0m00.00s || 112 ko | +0.00% | +0.02% 0m00.47s | 482464 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo | 0m00.47s | 482384 ko || +0m00.00s || 80 ko | +0.00% | +0.01% 0m00.42s | 381876 ko | Rewriter/Util/Sum.vo | 0m00.43s | 381932 ko || -0m00.01s || -56 ko | -2.32% | -0.01% 0m00.41s | 424548 ko | Rewriter/Language/Reify.vo | 0m00.36s | 424428 ko || +0m00.04s || 120 ko | +13.88% | +0.02% 0m00.33s | 412068 ko | Rewriter/Util/Strings/ParseArithmetic.vo | 0m00.35s | 412208 ko || -0m00.01s || -140 ko | -5.71% | -0.03% 0m00.29s | 336492 ko | Rewriter/Util/MSetPositive/Equality.vo | 0m00.30s | 336560 ko || -0m00.01s || -68 ko | -3.33% | -0.02% 0m00.29s | 372040 ko | Rewriter/Util/MSetPositive/Facts.vo | 0m00.33s | 372168 ko || -0m00.04s || -128 ko | -12.12% | -0.03% 0m00.28s | 387808 ko | Rewriter/Language/UnderLets.vo | 0m00.33s | 387632 ko || -0m00.04s || 176 ko | -15.15% | +0.04% 0m00.25s | 307788 ko | Rewriter/Language/PreLemmas.vo | 0m00.28s | 307888 ko || -0m00.03s || -100 ko | -10.71% | -0.03% 0m00.25s | 345464 ko | Rewriter/Util/ListUtil/SetoidList.vo | 0m00.24s | 345480 ko || +0m00.01s || -16 ko | +4.16% | -0.00% 0m00.23s | 314084 ko | Rewriter/Util/Option.vo | 0m00.26s | 314124 ko || -0m00.03s || -40 ko | -11.53% | -0.01% 0m00.23s | 367756 ko | Rewriter/Util/Strings/String.vo | 0m00.26s | 367772 ko || -0m00.03s || -16 ko | -11.53% | -0.00% 0m00.21s | 323684 ko | Rewriter/Language/UnderLetsCacheProofs.vo | 0m00.24s | 323216 ko || -0m00.03s || 468 ko | -12.50% | +0.14% 0m00.19s | 303140 ko | Rewriter/Util/FMapPositive/Equality.vo | 0m00.19s | 303024 ko || +0m00.00s || 116 ko | +0.00% | +0.03% 0m00.18s | 267900 ko | Rewriter/Util/Strings/Parse/Common.vo | 0m00.18s | 268108 ko || +0m00.00s || -208 ko | +0.00% | -0.07% 0m00.17s | 251988 ko | Rewriter/Util/Strings/Decimal.vo | 0m00.13s | 252092 ko || +0m00.04s || -104 ko | +30.76% | -0.04% 0m00.16s | 209704 ko | Rewriter/Util/Strings/Ascii.vo | 0m00.13s | 209556 ko || +0m00.03s || 148 ko | +23.07% | +0.07% 0m00.14s | 263380 ko | Rewriter/Util/Prod.vo | 0m00.13s | 263480 ko || +0m00.01s || -100 ko | +7.69% | -0.03% 0m00.13s | 257012 ko | Rewriter/Util/OptionList.vo | 0m00.19s | 257132 ko || -0m00.06s || -120 ko | -31.57% | -0.04% 0m00.11s | 115068 ko | Rewriter/Language/Pre.vo | 0m00.09s | 114828 ko || +0m00.02s || 240 ko | +22.22% | +0.20% 0m00.11s | 195496 ko | Rewriter/Util/PrimitiveProd.vo | 0m00.11s | 195572 ko || +0m00.00s || -76 ko | +0.00% | -0.03% 0m00.11s | 220420 ko | Rewriter/Util/Sigma.vo | 0m00.14s | 220324 ko || -0m00.03s || 96 ko | -21.42% | +0.04% 0m00.10s | 111776 ko | Rewriter/Util/PrimitiveHList.vo | 0m00.08s | 111708 ko || +0m00.02s || 68 ko | +25.00% | +0.06% 0m00.10s | 161712 ko | Rewriter/Util/PrimitiveSigma.vo | 0m00.11s | 161512 ko || -0m00.00s || 200 ko | -9.09% | +0.12% 0m00.09s | 113096 ko | Rewriter/Language/PreCommon.vo | 0m00.07s | 112976 ko || +0m00.01s || 120 ko | +28.57% | +0.10% 0m00.08s | 114432 ko | Rewriter/Util/Sigma/Related.vo | 0m00.05s | 114516 ko || +0m00.03s || -84 ko | +60.00% | -0.07% 0m00.08s | 30616 ko | Rewriter/Util/plugins/rewriter_build.cmx | 0m00.08s | 30592 ko || +0m00.00s || 24 ko | +0.00% | +0.07% 0m00.07s | 129832 ko | Rewriter/Util/Bool.vo | 0m00.07s | 129668 ko || +0m00.00s || 164 ko | +0.00% | +0.12% 0m00.07s | 136472 ko | Rewriter/Util/Equality.vo | 0m00.07s | 136508 ko || +0m00.00s || -36 ko | +0.00% | -0.02% 0m00.07s | 74068 ko | Rewriter/Util/Tactics/BreakMatch.vo | 0m00.06s | 74300 ko || +0m00.01s || -232 ko | +16.66% | -0.31% 0m00.07s | 95092 ko | Rewriter/Util/Tactics/RewriteHyp.vo | 0m00.03s | 95280 ko || +0m00.04s || -188 ko | +133.33% | -0.19% 0m00.07s | 77992 ko | Rewriter/Util/Tactics2/ReplaceByPattern.vo | 0m00.03s | 77956 ko || +0m00.04s || 36 ko | +133.33% | +0.04% 0m00.06s | 131564 ko | Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.vo | 0m00.09s | 131492 ko || -0m00.03s || 72 ko | -33.33% | +0.05% 0m00.06s | 99512 ko | Rewriter/Util/Logic/ExistsEqAnd.vo | 0m00.05s | 99488 ko || +0m00.00s || 24 ko | +19.99% | +0.02% 0m00.06s | 77760 ko | Rewriter/Util/Tactics2/Constr.vo | 0m00.06s | 77700 ko || +0m00.00s || 60 ko | +0.00% | +0.07% 0m00.06s | 77868 ko | Rewriter/Util/Tactics2/DecomposeLambda.vo | 0m00.06s | 77904 ko || +0m00.00s || -36 ko | +0.00% | -0.04% 0m00.06s | 26956 ko | Rewriter/Util/plugins/rewriter_build_plugin.cmx | 0m00.08s | 26916 ko || -0m00.02s || 40 ko | -25.00% | +0.14% 0m00.06s | 52920 ko | Rewriter/Util/plugins/rewriter_build_plugin.cmxa | 0m00.02s | 52560 ko || +0m00.03s || 360 ko | +199.99% | +0.68% 0m00.06s | 21100 ko | Rewriter/Util/plugins/rewriter_build_plugin.cmxs | 0m00.06s | 21132 ko || +0m00.00s || -32 ko | +0.00% | -0.15% 0m00.05s | 70096 ko | Rewriter/Util/InductiveHList.vo | 0m00.01s | 70200 ko || +0m00.04s || -104 ko | +400.00% | -0.14% 0m00.05s | 69008 ko | Rewriter/Util/Tactics/CPSId.vo | 0m00.05s | 68692 ko || +0m00.00s || 316 ko | +0.00% | +0.46% 0m00.05s | 70984 ko | Rewriter/Util/Tactics/SpecializeAllWays.vo | 0m00.03s | 71040 ko || +0m00.02s || -56 ko | +66.66% | -0.07% 0m00.05s | 72196 ko | Rewriter/Util/Tactics/SplitInContext.vo | 0m00.01s | 72016 ko || +0m00.04s || 180 ko | +400.00% | +0.24% 0m00.05s | 77288 ko | Rewriter/Util/Tactics2/Array.vo | 0m00.05s | 77364 ko || +0m00.00s || -76 ko | +0.00% | -0.09% 0m00.05s | 77384 ko | Rewriter/Util/Tactics2/Constr/Unsafe/MakeAbbreviations.vo | 0m00.04s | 77384 ko || +0m00.01s || 0 ko | +25.00% | +0.00% 0m00.05s | 77548 ko | Rewriter/Util/Tactics2/Head.vo | 0m00.03s | 77444 ko || +0m00.02s || 104 ko | +66.66% | +0.13% 0m00.05s | 77628 ko | Rewriter/Util/Tactics2/Ident.vo | 0m00.07s | 77656 ko || -0m00.02s || -28 ko | -28.57% | -0.03% 0m00.05s | 77392 ko | Rewriter/Util/Tactics2/List.vo | 0m00.04s | 77372 ko || +0m00.01s || 20 ko | +25.00% | +0.02% 0m00.05s | 77408 ko | Rewriter/Util/Tactics2/Option.vo | 0m00.03s | 77348 ko || +0m00.02s || 60 ko | +66.66% | +0.07% 0m00.05s | 77452 ko | Rewriter/Util/Tactics2/String.vo | 0m00.05s | 77440 ko || +0m00.00s || 12 ko | +0.00% | +0.01% 0m00.05s | 68912 ko | Rewriter/Util/TypeList.vo | 0m00.03s | 68912 ko || +0m00.02s || 0 ko | +66.66% | +0.00% 0m00.04s | 75740 ko | Rewriter/Util/Bool/Equality.vo | 0m00.03s | 75740 ko || +0m00.01s || 0 ko | +33.33% | +0.00% 0m00.04s | 78652 ko | Rewriter/Util/Comparison.vo | 0m00.02s | 78552 ko || +0m00.02s || 100 ko | +100.00% | +0.12% 0m00.04s | 84316 ko | Rewriter/Util/Logic/ProdForall.vo | 0m00.04s | 84472 ko || +0m00.00s || -156 ko | +0.00% | -0.18% 0m00.04s | 77708 ko | Rewriter/Util/Tactics/DestructHead.vo | 0m00.02s | 77768 ko || +0m00.02s || -60 ko | +100.00% | -0.07% 0m00.04s | 71032 ko | Rewriter/Util/Tactics/FindHyp.vo | 0m00.05s | 71236 ko || -0m00.01s || -204 ko | -20.00% | -0.28% 0m00.04s | 70716 ko | Rewriter/Util/Tactics/Head.vo | 0m00.03s | 70776 ko || +0m00.01s || -60 ko | +33.33% | -0.08% 0m00.04s | 67900 ko | Rewriter/Util/Tactics/SetoidSubst.vo | 0m00.02s | 68052 ko || +0m00.02s || -152 ko | +100.00% | -0.22% 0m00.04s | 71608 ko | Rewriter/Util/Tactics/UniquePose.vo | 0m00.03s | 71708 ko || +0m00.01s || -100 ko | +33.33% | -0.13% 0m00.04s | 78696 ko | Rewriter/Util/Tactics2/FixNotationsForPerformance.vo | 0m00.03s | 78712 ko || +0m00.01s || -16 ko | +33.33% | -0.02% 0m00.04s | 77644 ko | Rewriter/Util/Tactics2/HeadReference.vo | 0m00.05s | 77656 ko || -0m00.01s || -12 ko | -20.00% | -0.01% 0m00.04s | 77348 ko | Rewriter/Util/Tactics2/Iterate.vo | 0m00.05s | 77332 ko || -0m00.01s || 16 ko | -20.00% | +0.02% 0m00.04s | 77348 ko | Rewriter/Util/Tactics2/Message.vo | 0m00.05s | 77424 ko || -0m00.01s || -76 ko | -20.00% | -0.09% 0m00.04s | 19716 ko | Rewriter/Util/plugins/definition_by_tactic_plugin.cmxs | 0m00.02s | 19724 ko || +0m00.02s || -8 ko | +100.00% | -0.04% 0m00.04s | 52712 ko | Rewriter/Util/plugins/ltac2_extra_plugin.cmxa | 0m00.04s | 52436 ko || +0m00.00s || 276 ko | +0.00% | +0.52% 0m00.04s | 53276 ko | Rewriter/Util/plugins/strategy_tactic_plugin.cmxa | 0m00.04s | 52788 ko || +0m00.00s || 488 ko | +0.00% | +0.92% 0m00.03s | 77720 ko | Rewriter/Util/CPSNotations.vo | 0m00.07s | 77832 ko || -0m00.04s || -112 ko | -57.14% | -0.14% 0m00.03s | 85764 ko | Rewriter/Util/IffT.vo | 0m00.03s | 85896 ko || +0m00.00s || -132 ko | +0.00% | -0.15% 0m00.03s | 98240 ko | Rewriter/Util/LetIn.vo | 0m00.03s | 98092 ko || +0m00.00s || 148 ko | +0.00% | +0.15% 0m00.03s | 82412 ko | Rewriter/Util/Notations.vo | 0m00.02s | 82316 ko || +0m00.00s || 96 ko | +49.99% | +0.11% 0m00.03s | 87472 ko | Rewriter/Util/Pointed.vo | 0m00.05s | 87468 ko || -0m00.02s || 4 ko | -40.00% | +0.00% 0m00.03s | 69236 ko | Rewriter/Util/Tactics/CacheTerm.vo | 0m00.04s | 69284 ko || -0m00.01s || -48 ko | -25.00% | -0.06% 0m00.03s | 66848 ko | Rewriter/Util/Tactics/ConstrFail.vo | 0m00.04s | 66824 ko || -0m00.01s || 24 ko | -25.00% | +0.03% 0m00.03s | 66876 ko | Rewriter/Util/Tactics/Contains.vo | 0m00.03s | 66808 ko || +0m00.00s || 68 ko | +0.00% | +0.10% 0m00.03s | 75772 ko | Rewriter/Util/Tactics/DebugPrint.vo | 0m00.03s | 75796 ko || +0m00.00s || -24 ko | +0.00% | -0.03% 0m00.03s | 71144 ko | Rewriter/Util/Tactics/DoWithHyp.vo | 0m00.04s | 71204 ko || -0m00.01s || -60 ko | -25.00% | -0.08% 0m00.03s | 66840 ko | Rewriter/Util/Tactics/EvarNormalize.vo | 0m00.04s | 66924 ko || -0m00.01s || -84 ko | -25.00% | -0.12% 0m00.03s | 66820 ko | Rewriter/Util/Tactics/GetGoal.vo | 0m00.03s | 66756 ko || +0m00.00s || 64 ko | +0.00% | +0.09% 0m00.03s | 71152 ko | Rewriter/Util/Tactics/HeadUnderBinders.vo | 0m00.03s | 71044 ko || +0m00.00s || 108 ko | +0.00% | +0.15% 0m00.03s | 66900 ko | Rewriter/Util/Tactics/Not.vo | 0m00.02s | 66824 ko || +0m00.00s || 76 ko | +49.99% | +0.11% 0m00.03s | 70940 ko | Rewriter/Util/Tactics/RunTacticAsConstr.vo | 0m00.01s | 71096 ko || +0m00.01s || -156 ko | +199.99% | -0.21% 0m00.03s | 66732 ko | Rewriter/Util/Tactics/Test.vo | 0m00.05s | 66716 ko || -0m00.02s || 16 ko | -40.00% | +0.02% 0m00.03s | 67784 ko | Rewriter/Util/Tactics/TransparentAssert.vo | 0m00.02s | 67560 ko || +0m00.00s || 224 ko | +49.99% | +0.33% 0m00.03s | 77464 ko | Rewriter/Util/Tactics2/Char.vo | 0m00.04s | 77428 ko || -0m00.01s || 36 ko | -25.00% | +0.04% 0m00.03s | 77472 ko | Rewriter/Util/Tactics2/InFreshContext.vo | 0m00.04s | 77504 ko || -0m00.01s || -32 ko | -25.00% | -0.04% 0m00.03s | 77424 ko | Rewriter/Util/Tactics2/Ltac1.vo | 0m00.05s | 77320 ko || -0m00.02s || 104 ko | -40.00% | +0.13% 0m00.03s | 77356 ko | Rewriter/Util/Tactics2/Notations.vo | 0m00.04s | 77480 ko || -0m00.01s || -124 ko | -25.00% | -0.16% 0m00.03s | 52900 ko | Rewriter/Util/plugins/definition_by_tactic_plugin.cmxa | 0m00.04s | 53200 ko || -0m00.01s || -300 ko | -25.00% | -0.56% 0m00.03s | 20384 ko | Rewriter/Util/plugins/inductive_from_elim.cmi | 0m00.02s | 20148 ko || +0m00.00s || 236 ko | +49.99% | +1.17% 0m00.03s | 28460 ko | Rewriter/Util/plugins/inductive_from_elim.cmx | 0m00.04s | 28484 ko || -0m00.01s || -24 ko | -25.00% | -0.08% 0m00.03s | 24220 ko | Rewriter/Util/plugins/inductive_from_elim_plugin.cmx | 0m00.03s | 24008 ko || +0m00.00s || 212 ko | +0.00% | +0.88% 0m00.03s | 19540 ko | Rewriter/Util/plugins/inductive_from_elim_plugin.cmxs | 0m00.02s | 19688 ko || +0m00.00s || -148 ko | +49.99% | -0.75% 0m00.03s | 19632 ko | Rewriter/Util/plugins/ltac2_extra_plugin.cmxs | 0m00.01s | 19756 ko || +0m00.01s || -124 ko | +199.99% | -0.62% 0m00.02s | 76936 ko | Rewriter/Util/FixCoqMistakes.vo | 0m00.03s | 76976 ko || -0m00.00s || -40 ko | -33.33% | -0.05% 0m00.02s | 95764 ko | Rewriter/Util/HProp.vo | 0m00.05s | 95824 ko || -0m00.03s || -60 ko | -60.00% | -0.06% 0m00.02s | 67804 ko | Rewriter/Util/Isomorphism.vo | 0m00.03s | 67652 ko || -0m00.00s || 152 ko | -33.33% | +0.22% 0m00.02s | 70672 ko | Rewriter/Util/Tactics/AssertSucceedsPreserveError.vo | 0m00.05s | 70804 ko || -0m00.03s || -132 ko | -60.00% | -0.18% 0m00.02s | 66968 ko | Rewriter/Util/Tactics/ClearFree.vo | 0m00.02s | 66884 ko || +0m00.00s || 84 ko | +0.00% | +0.12% 0m00.02s | 72272 ko | Rewriter/Util/Tactics/DestructHyps.vo | 0m00.05s | 72296 ko || -0m00.03s || -24 ko | -60.00% | -0.03% 0m00.02s | 71536 ko | Rewriter/Util/Tactics/SpecializeBy.vo | 0m00.03s | 71440 ko || -0m00.00s || 96 ko | -33.33% | +0.13% 0m00.02s | 66928 ko | Rewriter/Util/Tactics/SubstEvars.vo | 0m00.02s | 66760 ko || +0m00.00s || 168 ko | +0.00% | +0.25% 0m00.02s | 67116 ko | Rewriter/Util/Tactics/WarnIfGoalsRemain.vo | 0m00.03s | 66940 ko || -0m00.00s || 176 ko | -33.33% | +0.26% 0m00.02s | 77280 ko | Rewriter/Util/Tactics2/Proj.vo | 0m00.03s | 77468 ko || -0m00.00s || -188 ko | -33.33% | -0.24% 0m00.02s | 20456 ko | Rewriter/Util/plugins/definition_by_tactic.cmi | 0m00.02s | 20608 ko || +0m00.00s || -152 ko | +0.00% | -0.73% 0m00.02s | 26476 ko | Rewriter/Util/plugins/definition_by_tactic.cmx | 0m00.03s | 26380 ko || -0m00.00s || 96 ko | -33.33% | +0.36% 0m00.02s | 22920 ko | Rewriter/Util/plugins/ltac2_extra.cmx | 0m00.03s | 22996 ko || -0m00.00s || -76 ko | -33.33% | -0.33% 0m00.02s | 19356 ko | Rewriter/Util/plugins/rewriter_build.cmi | 0m00.02s | 19160 ko || +0m00.00s || 196 ko | +0.00% | +1.02% 0m00.02s | 23348 ko | Rewriter/Util/plugins/strategy_tactic_plugin.cmx | 0m00.02s | 23268 ko || +0m00.00s || 80 ko | +0.00% | +0.34% 0m00.02s | 19312 ko | Rewriter/Util/plugins/strategy_tactic_plugin.cmxs | 0m00.03s | 19272 ko || -0m00.00s || 40 ko | -33.33% | +0.20% 0m00.01s | 66880 ko | Rewriter/Util/Tactics/PrintContext.vo | 0m00.02s | 66948 ko || -0m00.01s || -68 ko | -50.00% | -0.10% 0m00.01s | 67196 ko | Rewriter/Util/Tactics/PrintGoal.vo | 0m00.02s | 67032 ko || -0m00.01s || 164 ko | -50.00% | +0.24% 0m00.01s | 77200 ko | Rewriter/Util/plugins/Ltac2Extra.vo | 0m00.04s | 77196 ko || -0m00.03s || 4 ko | -75.00% | +0.00% 0m00.01s | 66732 ko | Rewriter/Util/plugins/StrategyTactic.vo | 0m00.02s | 66716 ko || -0m00.01s || 16 ko | -50.00% | +0.02% 0m00.01s | 25396 ko | Rewriter/Util/plugins/definition_by_tactic_plugin.cmx | 0m00.02s | 25316 ko || -0m00.01s || 80 ko | -50.00% | +0.31% 0m00.01s | 53388 ko | Rewriter/Util/plugins/inductive_from_elim_plugin.cmxa | 0m00.02s | 52852 ko || -0m00.01s || 536 ko | -50.00% | +1.01% 0m00.01s | 17176 ko | Rewriter/Util/plugins/ltac2_extra.cmi | 0m00.02s | 17280 ko || -0m00.01s || -104 ko | -50.00% | -0.60% 0m00.01s | 20184 ko | Rewriter/Util/plugins/ltac2_extra_plugin.cmx | 0m00.02s | 20032 ko || -0m00.01s || 152 ko | -50.00% | +0.75% 0m00.01s | 19200 ko | Rewriter/Util/plugins/strategy_tactic.cmi | 0m00.01s | 19248 ko || +0m00.00s || -48 ko | +0.00% | -0.24% 0m00.01s | 22632 ko | Rewriter/Util/plugins/strategy_tactic.cmx | 0m00.02s | 22684 ko || -0m00.01s || -52 ko | -50.00% | -0.22% 0m00.00s | 66280 ko | Rewriter/Util/GlobalSettings.vo | 0m00.02s | 66200 ko || -0m00.02s || 80 ko | -100.00% | +0.12% 0m00.00s | 66712 ko | Rewriter/Util/Tactics/SetEvars.vo | 0m00.01s | 66844 ko || -0m00.01s || -132 ko | -100.00% | -0.19% ```

--- src/Rewriter/Language/UnderLets.v | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Rewriter/Language/UnderLets.v b/src/Rewriter/Language/UnderLets.v index 78796f201..0419c80ef 100644 --- a/src/Rewriter/Language/UnderLets.v +++ b/src/Rewriter/Language/UnderLets.v @@ -263,4 +263,5 @@ Module Compilers. End reify. End UnderLets. Export UnderLets.Notations. + Global Strategy -1000 [UnderLets.to_expr]. End Compilers.