-
Notifications
You must be signed in to change notification settings - Fork 0
/
.Imp.aux
172 lines (172 loc) · 5.58 KB
/
.Imp.aux
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
COQAUX1 93a27baa22f2b2dca39b10ee9b79686d /home/rog0d/Escritorio/compiler_new/Imp.v
0 0 VernacProof "tac:no using:no"
3368 3372 proof_build_time "0.000"
0 0 test_aeval1 "0.000"
3355 3367 context_used ""
3368 3372 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4779 4783 proof_build_time "0.000"
0 0 test_optimize_0plus "0.000"
4766 4778 context_used ""
4779 4783 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5722 5726 proof_build_time "0.017"
0 0 optimize_0plus_sound "0.017"
5708 5720 context_used ""
5722 5726 proof_check_time "0.006"
0 0 VernacProof "tac:no using:no"
8219 8223 proof_build_time "0.002"
0 0 foo "0.002"
8161 8173 context_used ""
8219 8223 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
8546 8550 proof_build_time "0.001"
0 0 foo' "0.001"
8397 8545 context_used ""
8546 8550 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
9389 9393 proof_build_time "0.010"
0 0 optimize_0plus_sound' "0.010"
9335 9386 context_used ""
9389 9393 proof_check_time "0.004"
0 0 VernacProof "tac:no using:no"
12021 12025 proof_build_time "0.010"
0 0 optimize_0plus_sound'' "0.010"
11968 12019 context_used ""
12021 12025 proof_check_time "0.004"
0 0 VernacProof "tac:no using:no"
16142 16146 proof_build_time "0.047"
0 0 optimize_0plus_sound''' "0.047"
16089 16140 context_used ""
16142 16146 proof_check_time "0.003"
0 0 VernacProof "tac:no using:no"
20349 20353 proof_build_time "0.011"
0 0 aeval_iff_aevalR "0.011"
20335 20347 context_used ""
20349 20353 proof_check_time "0.005"
20720 20724 proof_build_time "0.004"
0 0 aeval_iff_aevalR' "0.004"
20620 20718 context_used ""
20720 20724 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
24572 24576 proof_build_time "0.001"
0 0 silly_presburger_formula "0.001"
24566 24570 context_used ""
24572 24576 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
27279 27283 proof_build_time "0.000"
0 0 beq_id_refl "0.000"
27258 27277 context_used ""
27279 27283 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
27630 27639 proof_build_time "0.000"
0 0 beq_id_eq "0.000"
27630 27639 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
27798 27807 proof_build_time "0.000"
0 0 beq_id_false_not_eq "0.000"
27798 27807 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
27966 27975 proof_build_time "0.000"
0 0 not_eq_beq_id_false "0.000"
27966 27975 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
28119 28128 proof_build_time "0.000"
0 0 beq_id_sym "0.000"
28119 28128 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
28725 28734 proof_build_time "0.000"
0 0 update_eq "0.000"
28725 28734 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
28913 28922 proof_build_time "0.000"
0 0 update_neq "0.000"
28913 28922 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
29199 29208 proof_build_time "0.000"
0 0 update_example "0.000"
29199 29208 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
29396 29405 proof_build_time "0.000"
0 0 update_shadow "0.000"
29396 29405 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
29581 29590 proof_build_time "0.000"
0 0 update_same "0.000"
29581 29590 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
29822 29831 proof_build_time "0.000"
0 0 update_permute "0.000"
29822 29831 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
32176 32180 proof_build_time "0.000"
0 0 aexp1 "0.000"
32163 32175 context_used ""
32176 32180 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
32313 32317 proof_build_time "0.000"
0 0 bexp1 "0.000"
32300 32312 context_used ""
32313 32317 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
41976 41980 proof_build_time "0.002"
0 0 ceval_example1 "0.002"
41962 41974 context_used ""
41976 41980 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
42186 42195 proof_build_time "0.000"
0 0 ceval_example2 "0.000"
42186 42195 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
45992 45996 proof_build_time "0.024"
0 0 ceval_step__ceval "0.024"
45978 45990 context_used ""
45992 45996 proof_check_time "0.009"
0 0 VernacProof "tac:no using:no"
47972 47976 proof_build_time "0.019"
0 0 ceval_step_more "0.019"
47953 47970 context_used ""
47972 47976 proof_check_time "0.007"
0 0 VernacProof "tac:no using:no"
48348 48357 proof_build_time "0.003"
0 0 ceval__ceval_step "0.003"
48348 48357 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
48577 48581 proof_build_time "0.000"
0 0 ceval_and_ceval_step_coincide "0.000"
48552 48576 context_used ""
48577 48581 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
50621 50625 proof_build_time "0.049"
0 0 ceval_deterministic "0.049"
50608 50619 context_used ""
50621 50625 proof_check_time "0.028"
0 0 VernacProof "tac:no using:no"
51198 51202 proof_build_time "0.003"
0 0 ceval_deterministic' "0.003"
51192 51196 context_used ""
51198 51202 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
51853 51857 proof_build_time "0.004"
0 0 plus2_spec "0.004"
51835 51851 context_used ""
51853 51857 proof_check_time "0.002"
0 0 VernacProof "tac:no using:no"
52432 52441 proof_build_time "0.000"
0 0 loop_never_stops "0.000"
52432 52441 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
53207 53216 proof_build_time "0.000"
0 0 no_whiles_eqv "0.000"
53207 53216 proof_check_time "0.000"
57286 57295 proof_build_time "0.000"
0 0 s_execute1 "0.000"
57286 57295 proof_check_time "0.000"
57431 57440 proof_build_time "0.000"
0 0 s_execute2 "0.000"
57431 57440 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
58236 58245 proof_build_time "0.000"
0 0 s_compile_correct "0.000"
58236 58245 proof_check_time "0.000"
0 0 vo_compile_time "0.520"