diff options
Diffstat (limited to 'test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.expected')
| -rw-r--r-- | test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.expected | 398 |
1 files changed, 398 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.expected new file mode 100644 index 0000000000..0fb57a1406 --- /dev/null +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/007-no-output-sync/time-of-build.log.expected @@ -0,0 +1,398 @@ + 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 |