1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
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
|
