Time | Peak Mem | File Name ------------------------------------------------------------- 29m02.87s | 1136588 ko | Total Time / Peak Mem ------------------------------------------------------------- 2m19.40s | 1007764 ko | PCUICSafeConversion.vo 1m59.92s | 1136588 ko | PCUICSafeReduce.vo 1m34.58s | 849824 ko | PCUICParallelReductionConfluence.vo 1m26.21s | 1038900 ko | erasure_live_test.vo 1m20.36s | 975764 ko | PCUICSR.vo 0m56.51s | 896928 ko | bugkncst.vo 0m56.17s | 1113548 ko | ErasureCorrectness.vo 0m56.09s | 958816 ko | PCUICSafeChecker.vo 0m51.78s | 809012 ko | Typing.vo 0m42.82s | 727688 ko | PCUICTyping.vo 0m39.21s | 1012876 ko | ErasureFunction.vo 0m39.04s | 790088 ko | PCUICEquality.vo 0m38.12s | 657100 ko | PCUICSigmaCalculus.vo 0m34.44s | 742788 ko | PCUICConfluence.vo 0m29.65s | 750296 ko | PCUICConversion.vo 0m28.26s | 779308 ko | PCUICParallelReduction.vo 0m28.24s | 723216 ko | PCUICPosition.vo 0m27.93s | 621392 ko | Substitution.vo 0m26.28s | 597996 ko | PCUICLiftSubst.vo 0m26.11s | 959132 ko | PCUICPrincipality.vo 0m25.86s | 857128 ko | times_bool_fun.vo 0m25.65s | 673140 ko | PCUICSubstitution.vo 0m23.99s | 654592 ko | PCUICClosed.vo 0m23.42s | 685852 ko | PCUICWeakening.vo 0m23.34s | 854428 ko | SafeErasureFunction.vo 0m22.85s | 706592 ko | PCUICSpine.vo 0m21.55s | 603616 ko | Closed.vo 0m19.93s | 581920 ko | tauto.vo 0m19.08s | 683776 ko | PCUICInductives.vo 0m17.91s | 741808 ko | param_original.vo 0m15.64s | 579100 ko | Weakening.vo 0m14.98s | 623196 ko | PCUICNameless.vo 0m13.39s | 794032 ko | ESubstitution.vo 0m13.16s | 641024 ko | TemplateToPCUICCorrectness.vo 0m11.81s | 532016 ko | LiftSubst.vo 0m11.54s | 589944 ko | PCUICWcbvEval.vo 0m10.41s | 621644 ko | PCUICUnivSubstitution.vo 0m10.39s | 661964 ko | PCUICInductiveInversion.vo 0m10.08s | 521520 ko | ELiftSubst.vo 0m09.58s | 684644 ko | PCUICAlpha.vo 0m09.35s | 622488 ko | PCUICInversion.vo 0m08.74s | 629108 ko | PCUICContextConversion.vo 0m08.61s | 892080 ko | param_generous_packed.vo 0m08.05s | 556676 ko | TypingWf.vo 0m07.84s | 608576 ko | PCUICToTemplateCorrectness.vo 0m07.75s | 625664 ko | PCUICArities.vo 0m07.64s | 646256 ko | PCUICElimination.vo 0m07.23s | 614752 ko | times_bool_fun2.vo 0m06.54s | 667924 ko | PCUICSafeLemmata.vo 0m06.33s | 615568 ko | PCUICContexts.vo 0m06.30s | 733700 ko | PCUICSafeRetyping.vo 0m06.16s | 583116 ko | PCUICReduction.vo 0m06.04s | 529900 ko | utils/MCCompare.vo 0m05.85s | 551516 ko | common/uGraph.vo 0m05.66s | 643396 ko | EArities.vo 0m04.94s | 533768 ko | WcbvEval.vo 0m04.90s | 501352 ko | vs.vo 0m04.72s | 498552 ko | utils/wGraph.vo 0m04.53s | 552364 ko | Reflect.vo 0m04.41s | 348856 ko | MiniHoTT.vo 0m04.38s | 571076 ko | PCUICWeakeningEnv.vo 0m04.23s | 531272 ko | Universes.vo 0m04.11s | 543956 ko | PCUICReflect.vo 0m04.00s | 555748 ko | Checker.vo 0m03.99s | 624912 ko | PCUICValidity.vo 0m03.99s | 806128 ko | SafeTemplateErasure.vo 0m03.85s | 520080 ko | EWcbvEval.vo 0m03.42s | 350716 ko | MiniHoTT_paths.vo 0m03.39s | 741428 ko | Prelim.vo 0m03.34s | 586388 ko | PCUICGeneration.vo 0m03.33s | 533884 ko | PCUICUnivSubst.vo 0m03.11s | 561316 ko | Extraction.vo 0m03.11s | 490756 ko | UnivSubst.vo 0m02.89s | 726228 ko | safechecker_test.vo 0m02.80s | 512292 ko | WeakeningEnv.vo 0m02.78s | 543424 ko | PCUICAstUtils.vo 0m02.78s | 465984 ko | utils/All_Forall.vo 0m02.67s | 729072 ko | EInversion.vo 0m02.42s | 703592 ko | SafeTemplateChecker.vo 0m02.27s | 558304 ko | TypingTests.vo 0m02.12s | 630488 ko | PCUICSN.vo 0m01.93s | 556444 ko | param_binary.vo 0m01.85s | 561876 ko | PCUICCumulativity.vo 0m01.82s | 554420 ko | translation_utils.vo 0m01.77s | 491968 ko | EnvironmentTyping.vo 0m01.75s | 598288 ko | PCUICCtxShape.vo 0m01.69s | 514692 ko | Generation.vo 0m01.62s | 512080 ko | bug5.vo 0m01.58s | 589768 ko | PCUICRetyping.vo 0m01.57s | 617808 ko | Extract.vo 0m01.56s | 527740 ko | demo.vo 0m01.55s | 562424 ko | PCUICCSubst.vo 0m01.49s | 553352 ko | param_cheap_packed.vo 0m01.47s | 527440 ko | PCUICUtils.vo 0m01.47s | 452340 ko | utils/MCList.vo 0m01.44s | 503484 ko | PCUICSize.vo 0m01.42s | 619396 ko | EAll.vo 0m01.37s | 551200 ko | PCUICNormal.vo 0m01.35s | 526276 ko | modules_sections.vo 0m01.34s | 549492 ko | standard_model.vo 0m01.30s | 551364 ko | PCUICPretty.vo 0m01.29s | 545736 ko | All.vo 0m01.21s | 524028 ko | proj.vo 0m01.21s | 513888 ko | test/test.vo 0m01.18s | 486324 ko | Induction.vo 0m01.13s | 524144 ko | add_constructor.vo 0m01.11s | 549776 ko | PCUICChecker.vo 0m01.10s | 487520 ko | EAstUtils.vo 0m01.10s | 484172 ko | Environment.vo 0m01.10s | 543584 ko | erasure_test.vo 0m01.09s | 525128 ko | order_rec.vo 0m01.05s | 512080 ko | ECSubst.vo 0m01.05s | 489932 ko | WfInv.vo 0m01.05s | 522968 ko | issue28.vo 0m01.04s | 527408 ko | PCUICToTemplate.vo 0m01.03s | 510284 ko | bug1.vo 0m01.03s | 522996 ko | run_in_tactic.vo 0m01.03s | 522248 ko | unfold.vo 0m01.02s | 522688 ko | issue27.vo 0m01.01s | 524932 ko | tmVariable.vo 0m01.00s | 485664 ko | AstUtils.vo 0m00.99s | 522992 ko | univ.vo 0m00.98s | 522552 ko | tmInferInstance.vo 0m00.96s | 546928 ko | PCUICMetaTheory.vo 0m00.94s | 510368 ko | castprop.vo 0m00.94s | 500016 ko | opaque.vo 0m00.92s | 522724 ko | tmExistingInstance.vo 0m00.91s | 513348 ko | MyPlugin.vo 0m00.90s | 524140 ko | Retyping.vo 0m00.90s | 500080 ko | letin.vo 0m00.89s | 481312 ko | PCUICInduction.vo 0m00.89s | 500252 ko | bug7.vo 0m00.89s | 500068 ko | mutind.vo 0m00.88s | 500120 ko | case.vo 0m00.88s | 501748 ko | extractable.vo 0m00.87s | 486460 ko | Pretty.vo 0m00.86s | 500064 ko | sigma.vo 0m00.85s | 500408 ko | bug6.vo 0m00.84s | 497360 ko | Normal.vo 0m00.84s | 500436 ko | bug8.vo 0m00.82s | 498504 ko | Constants.vo 0m00.81s | 500380 ko | bug2.vo 0m00.81s | 500192 ko | cofix.vo 0m00.80s | 502088 ko | hnf_ctor.vo 0m00.79s | 479940 ko | Ast.vo 0m00.79s | 500100 ko | evars.vo 0m00.77s | 488076 ko | EPretty.vo 0m00.75s | 450728 ko | BasicAst.vo 0m00.75s | 477372 ko | PCUICAst.vo 0m00.73s | 487644 ko | ETyping.vo 0m00.73s | 481988 ko | TemplateMonad/Core.vo 0m00.72s | 477800 ko | EAst.vo 0m00.71s | 479012 ko | EInduction.vo 0m00.70s | 485084 ko | EWndEval.vo 0m00.70s | 481156 ko | TemplateMonad/Extractable.vo 0m00.69s | 482472 ko | TemplateToPCUIC.vo 0m00.60s | 433064 ko | PCUICCheckerCompleteness.vo 0m00.60s | 437492 ko | TemplateMonad/Common.vo 0m00.56s | 440168 ko | utils/MCOption.vo 0m00.54s | 420452 ko | TemplateMonad.vo 0m00.52s | 385340 ko | utils.vo 0m00.48s | 404556 ko | utils/MCArith.vo 0m00.42s | 339136 ko | utils/LibHypsNaming.vo 0m00.41s | 39160 ko | gen-src/universes0.cmx 0m00.33s | 45284 ko | pCUICSafeChecker.cmx 0m00.30s | 270156 ko | utils/MCString.vo 0m00.29s | 238116 ko | Loader.vo 0m00.27s | 43056 ko | pCUICSafeConversion.cmx 0m00.240s | N/A | denoter.cmx 0m00.19s | 34468 ko | gen-src/quoter.cmx 0m00.17s | 33044 ko | constr_quoter.cmx 0m00.15s | 25208 ko | gen-src/binPos.cmx 0m00.15s | 38520 ko | run_template_monad.cmx 0m00.14s | 31740 ko | constr_denoter.cmx 0m00.14s | 25372 ko | gen-src/all_Forall.cmx 0m00.14s | 149456 ko | monad_utils.vo 0m00.14s | 31636 ko | wGraph.cmx 0m00.13s | 23892 ko | gen-src/binPosDef.cmx 0m00.13s | 20232 ko | metacoq_erasure_plugin.cmxs 0m00.12s | 22784 ko | gen-src/binInt.cmx 0m00.11s | 31208 ko | erasureFunction.cmx 0m00.11s | 31632 ko | gen-src/metacoq_template_plugin.cmx 0m00.11s | 20224 ko | metacoq_safechecker_plugin.cmxs 0m00.11s | 30984 ko | uGraph0.cmx 0m00.10s | 28644 ko | eAst.cmx 0m00.10s | 33140 ko | g_template_coq.cmx 0m00.10s | 27364 ko | gen-src/ast_quoter.cmx 0m00.10s | 20796 ko | gen-src/binNat.cmx 0m00.10s | 18416 ko | gen-src/metacoq_template_plugin.cmxs 0m00.10s | 27228 ko | gen-src/myPlugin.cmx 0m00.10s | 26404 ko | gen-src/quoter.cmo 0m00.09s | 26992 ko | ePretty.cmx 0m00.09s | 35368 ko | g_metacoq_safechecker.cmx 0m00.09s | 24572 ko | gen-src/ast0.cmx 0m00.09s | 20020 ko | gen-src/hexadecimal.cmx 0m00.09s | 30504 ko | gen-src/run_extractable.cmx 0m00.09s | 29148 ko | pCUICPretty.cmx 0m00.09s | 29852 ko | safeErasureFunction.cmx 0m00.09s | 88348 ko | utils/MCProd.vo 0m00.08s | 27288 ko | gen-src/ast_denoter.cmx 0m00.08s | 24324 ko | gen-src/denoter.cmx 0m00.08s | 21352 ko | gen-src/mSetList.cmx 0m00.08s | 22020 ko | gen-src/pretty.cmx 0m00.08s | 32668 ko | metacoq_erasure_plugin.cmx 0m00.08s | 26392 ko | pCUICAstUtils.cmx 0m00.08s | 27752 ko | pCUICTyping.cmx 0m00.07s | 19912 ko | gen-src/peanoNat.cmx 0m00.07s | 27504 ko | gen-src/plugin_core.cmx 0m00.07s | 27792 ko | pCUICSafeReduce.cmx 0m00.07s | 30244 ko | safeTemplateErasure.cmx 0m00.06s | 24684 ko | eTyping.cmx 0m00.06s | 22652 ko | erasureFunction.cmi 0m00.06s | 27844 ko | g_demo_plugin.cmx 0m00.06s | 30052 ko | g_metacoq_erasure.cmx 0m00.06s | 25216 ko | mSetWeakList.cmx 0m00.06s | 30436 ko | metacoq_safechecker_plugin.cmx 0m00.06s | 26256 ko | pCUICEquality.cmx 0m00.06s | 26244 ko | pCUICLiftSubst.cmx 0m00.06s | 26048 ko | pCUICPosition.cmx 0m00.06s | 23232 ko | pCUICSafeConversion.cmi 0m00.06s | 27380 ko | pCUICSafeRetyping.cmx 0m00.06s | 25408 ko | safeTemplateChecker.cmx 0m00.06s | 26384 ko | templateToPCUIC.cmx 0m00.06s | 24780 ko | uGraph0.cmi 0m00.05s | 64048 ko | Lens.vo 0m00.05s | 24800 ko | eAstUtils.cmx 0m00.05s | 25192 ko | eLiftSubst.cmx 0m00.05s | 22440 ko | gen-src/ast_quoter.cmo 0m00.05s | 20324 ko | gen-src/mSetInterface.cmx 0m00.05s | 26032 ko | pCUICAst.cmx 0m00.05s | 25140 ko | pCUICChecker.cmx 0m00.05s | 24336 ko | pCUICReflect.cmx 0m00.05s | 24300 ko | pCUICSafeChecker.cmi 0m00.05s | 21556 ko | pCUICSafeReduce.cmi 0m00.05s | 25180 ko | pCUICUnivSubst.cmx 0m00.05s | 21660 ko | safeErasureFunction.cmi 0m00.05s | 23148 ko | safeTemplateErasure.cmi 0m00.05s | 21328 ko | templateToPCUIC.cmi 0m00.05s | 16040 ko | template_coq.cmxs 0m00.05s | 24076 ko | typing0.cmx 0m00.05s | 63096 ko | utils/MCPrelude.vo 0m00.05s | 68156 ko | utils/MCRelations.vo 0m00.05s | 22824 ko | wGraph.cmi 0m00.04s | 62716 ko | ExtractableLoader.vo 0m00.04s | 61716 ko | config.vo 0m00.04s | 22020 ko | constr_reification.cmx 0m00.04s | 21964 ko | demo_plugin.cmx 0m00.04s | 20540 ko | ePretty.cmi 0m00.04s | 23032 ko | extract.cmx 0m00.04s | 19608 ko | gen-src/astUtils.cmx 0m00.04s | 18780 ko | gen-src/extractable.cmx 0m00.04s | 22124 ko | gen-src/lens.cmx 0m00.04s | 19008 ko | gen-src/liftSubst.cmx 0m00.04s | 19600 ko | gen-src/mSetProperties.cmx 0m00.04s | 20208 ko | gen-src/myPlugin.cmi 0m00.04s | 18464 ko | gen-src/nat0.cmx 0m00.04s | 22136 ko | gen-src/tm_util.cmx 0m00.04s | 18504 ko | gen-src/universes0.cmi 0m00.04s | 20108 ko | mSetWeakList.cmi 0m00.04s | 22452 ko | monad_utils.cmx 0m00.04s | 21244 ko | pCUICAst.cmi 0m00.04s | 20412 ko | pCUICAstUtils.cmi 0m00.04s | 21236 ko | pCUICChecker.cmi 0m00.04s | 20560 ko | pCUICPretty.cmi 0m00.04s | 21400 ko | pCUICTyping.cmi 0m00.04s | 20348 ko | safeTemplateChecker.cmi 0m00.04s | 19228 ko | utils.cmi 0m00.04s | 22212 ko | utils.cmx 0m00.04s | 62924 ko | utils/MCEquality.vo 0m00.04s | 61384 ko | utils/MCSquash.vo 0m00.03s | 19340 ko | classes0.cmi 0m00.03s | 20908 ko | eAst.cmi 0m00.03s | 19496 ko | eAstUtils.cmi 0m00.03s | 20252 ko | eTyping.cmi 0m00.03s | 19268 ko | eqDecInstances.cmi 0m00.03s | 22196 ko | eqDecInstances.cmx 0m00.03s | 19396 ko | eqdepFacts.cmi 0m00.03s | 22072 ko | eqdepFacts.cmx 0m00.03s | 21060 ko | extract.cmi 0m00.03s | 18744 ko | gen-src/basicAst.cmx 0m00.03s | 17936 ko | gen-src/decimal.cmx 0m00.03s | 19716 ko | gen-src/environment.cmx 0m00.03s | 19172 ko | gen-src/lens.cmi 0m00.03s | 17796 ko | gen-src/list0.cmx 0m00.03s | 18548 ko | gen-src/univSubst0.cmx 0m00.03s | 19324 ko | init.cmi 0m00.03s | 22188 ko | init.cmx 0m00.03s | 19272 ko | monad_utils.cmi 0m00.03s | 20372 ko | pCUICEquality.cmi 0m00.03s | 20444 ko | pCUICLiftSubst.cmi 0m00.03s | 22044 ko | pCUICNormal.cmx 0m00.03s | 20488 ko | pCUICPosition.cmi 0m00.03s | 20240 ko | pCUICReflect.cmi 0m00.03s | 19348 ko | pCUICSafeLemmata.cmi 0m00.03s | 21604 ko | pCUICSafeRetyping.cmi 0m00.03s | 20308 ko | pCUICUnivSubst.cmi 0m00.03s | 21812 ko | tm_util.cmx 0m00.03s | 20300 ko | typing0.cmi 0m00.02s | 21960 ko | classes0.cmx 0m00.02s | 19300 ko | eLiftSubst.cmi 0m00.02s | 16900 ko | gen-src/ascii.cmx 0m00.02s | 16836 ko | gen-src/cRelationClasses.cmx 0m00.02s | 16420 ko | gen-src/common0.cmx 0m00.02s | 16472 ko | gen-src/mCString.cmx 0m00.02s | 15244 ko | gen-src/mSetInterface.cmi 0m00.02s | 15212 ko | gen-src/mSetProperties.cmi 0m00.02s | 17196 ko | gen-src/plugin_core.cmi 0m00.02s | 16332 ko | gen-src/specif.cmx 0m00.02s | 16504 ko | gen-src/string0.cmx 0m00.02s | 18448 ko | gen-src/tm_util.cmo 0m00.02s | 19224 ko | pCUICCumulativity.cmi 0m00.02s | 21940 ko | pCUICCumulativity.cmx 0m00.02s | 19304 ko | pCUICNormal.cmi 0m00.02s | 22084 ko | pCUICSafeLemmata.cmx 0m00.02s | 19220 ko | ssrbool.cmi 0m00.02s | 21912 ko | ssrbool.cmx 0m00.02s | 19956 ko | template_coq.cmx 0m00.01s | 14256 ko | demo_plugin.cmxs 0m00.01s | 14992 ko | gen-src/all_Forall.cmi 0m00.01s | 15204 ko | gen-src/ast0.cmi 0m00.01s | 14404 ko | gen-src/basicAst.cmi 0m00.01s | 13564 ko | gen-src/binInt.cmi 0m00.01s | 14264 ko | gen-src/binPos.cmi 0m00.01s | 15772 ko | gen-src/bool.cmx 0m00.01s | 13388 ko | gen-src/cRelationClasses.cmi 0m00.01s | 15536 ko | gen-src/compare_dec.cmx 0m00.01s | 16200 ko | gen-src/datatypes.cmx 0m00.01s | 14988 ko | gen-src/environment.cmi 0m00.01s | 15840 ko | gen-src/equalities.cmx 0m00.01s | 13404 ko | gen-src/list0.cmi 0m00.01s | 15672 ko | gen-src/mCCompare.cmx 0m00.01s | 16712 ko | gen-src/mCList.cmx 0m00.01s | 15708 ko | gen-src/mCProd.cmx 0m00.01s | 13748 ko | gen-src/mSetFacts.cmi 0m00.01s | 17012 ko | gen-src/mSetFacts.cmx 0m00.01s | 15760 ko | gen-src/mSetList.cmi 0m00.01s | 14056 ko | gen-src/metacoq_template_plugin.cmxa 0m00.01s | 15860 ko | gen-src/orderedType0.cmx 0m00.01s | 13748 ko | gen-src/orders.cmi 0m00.01s | 16768 ko | gen-src/orders.cmx 0m00.01s | 16032 ko | gen-src/ordersFacts.cmx 0m00.01s | 15844 ko | gen-src/ordersTac.cmx 0m00.01s | 11760 ko | gen-src/reification.cmo 0m00.01s | 14740 ko | gen-src/reification.cmx 0m00.01s | 13824 ko | gen-src/run_extractable.cmi 0m00.01s | 13460 ko | i 0m00.01s | 17068 ko | plugin_core.cmi 0m00.01s | 14796 ko | reification.cmx 0m00.00s | 13200 ko | demo_plugin.cmxa 0m00.00s | 12228 ko | gen-src/ascii.cmi 0m00.00s | 14040 ko | gen-src/astUtils.cmi 0m00.00s | 11244 ko | gen-src/basics.cmi 0m00.00s | 13444 ko | gen-src/binNat.cmi 0m00.00s | 11340 ko | gen-src/binNums.cmi 0m00.00s | 13536 ko | gen-src/binPosDef.cmi 0m00.00s | 11744 ko | gen-src/bool.cmi 0m00.00s | 13492 ko | gen-src/common0.cmi 0m00.00s | 11720 ko | gen-src/compare_dec.cmi 0m00.00s | 11112 ko | gen-src/config0.cmi 0m00.00s | 14648 ko | gen-src/config0.cmx 0m00.00s | 12948 ko | gen-src/datatypes.cmi 0m00.00s | 12404 ko | gen-src/decimal.cmi 0m00.00s | 13240 ko | gen-src/equalities.cmi 0m00.00s | 13580 ko | gen-src/extractable.cmi 0m00.00s | 13064 ko | gen-src/hexadecimal.cmi 0m00.00s | 13680 ko | gen-src/liftSubst.cmi 0m00.00s | 11524 ko | gen-src/logic0.cmi 0m00.00s | 15516 ko | gen-src/logic0.cmx 0m00.00s | 11644 ko | gen-src/mCCompare.cmi 0m00.00s | 13612 ko | gen-src/mCList.cmi 0m00.00s | 12200 ko | gen-src/mCOption.cmi 0m00.00s | 11228 ko | gen-src/mCPrelude.cmi 0m00.00s | 14368 ko | gen-src/mCPrelude.cmx 0m00.00s | 11620 ko | gen-src/mCProd.cmi 0m00.00s | 11080 ko | gen-src/mCRelations.cmi 0m00.00s | 14184 ko | gen-src/mCRelations.cmx 0m00.00s | 11712 ko | gen-src/mCString.cmi 0m00.00s | 13776 ko | gen-src/mSetDecide.cmi 0m00.00s | 11900 ko | gen-src/numeral.cmi 0m00.00s | 15820 ko | gen-src/numeral.cmx 0m00.00s | 12108 ko | gen-src/orderedType0.cmi 0m00.00s | 13444 ko | gen-src/ordersFacts.cmi 0m00.00s | 11760 ko | gen-src/ordersLists.cmi 0m00.00s | 15096 ko | gen-src/ordersLists.cmx 0m00.00s | 12464 ko | gen-src/ordersTac.cmi 0m00.00s | 15060 ko | gen-src/pretty.cmi 0m00.00s | 13160 ko | gen-src/specif.cmi 0m00.00s | 12236 ko | gen-src/string0.cmi 0m00.00s | 14128 ko | gen-src/univSubst0.cmi 0m00.00s | 13520 ko | metacoq_erasure_plugin.cmxa 0m00.00s | 13624 ko | metacoq_safechecker_plugin.cmxa 0m00.00s | 13148 ko | run_template_monad.cmi 0m00.00s | 13520 ko | template_coq.cmxa 0m00.00s | 15004 ko | template_monad.cmi