Compil/.SfLib.aux at main · roG0d/Compil · GitHub

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
COQAUX1 5e937f028e0cbad9efc574c9dc6030c1 /home/rog0d/Escritorio/compiler_new/SfLib.v
740 749 proof_build_time "0.000"
0 0 admit "0.000"
740 749 proof_check_time "0.003"
0 0 VernacProof "tac:no using:no"
2088 2092 proof_build_time "0.004"
0 0 andb_true_elim1 "0.004"
2074 2086 context_used ""
2088 2092 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
2200 2209 proof_build_time "0.000"
0 0 andb_true_elim2 "0.000"
2200 2209 proof_check_time "0.000"
2311 2320 proof_build_time "0.000"
0 0 beq_nat_sym "0.000"
2311 2320 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2861 2865 proof_build_time "0.002"
0 0 andb_true "0.002"
2847 2859 context_used ""
2861 2865 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
2993 3002 proof_build_time "0.000"
0 0 not_eq_beq_false "0.000"
2993 3002 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3111 3115 proof_build_time "0.000"
0 0 ex_falso_quodlibet "0.000"
3092 3109 context_used ""
3111 3115 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3208 3217 proof_build_time "0.000"
0 0 ev_not_ev_S "0.000"
3208 3217 proof_check_time "0.000"
3315 3324 proof_build_time "0.000"
0 0 ble_nat_true "0.000"
3315 3324 proof_check_time "0.000"
3427 3436 proof_build_time "0.000"
0 0 ble_nat_false "0.000"
3427 3436 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4484 4488 proof_build_time "0.001"
0 0 rsc_R "0.001"
4466 4481 context_used ""
4484 4488 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4683 4692 proof_build_time "0.000"
0 0 rsc_trans "0.000"
4683 4692 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
4988 4992 proof_build_time "0.001"
0 0 beq_id_refl "0.001"
4967 4986 context_used ""
4988 4992 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5163 5167 proof_build_time "0.001"
0 0 beq_id_eq "0.001"
5149 5161 context_used ""
5163 5167 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5378 5382 proof_build_time "0.002"
0 0 beq_id_false_not_eq "0.002"
5364 5376 context_used ""
5378 5382 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
5619 5623 proof_build_time "0.002"
0 0 not_eq_beq_id_false "0.002"
5606 5617 context_used ""
5619 5623 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
5758 5762 proof_build_time "0.001"
0 0 beq_id_sym "0.001"
5739 5757 context_used ""
5758 5762 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6153 6157 proof_build_time "0.001"
0 0 extend_eq "0.001"
6147 6152 context_used ""
6153 6157 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
6328 6332 proof_build_time "0.001"
0 0 extend_neq "0.001"
6322 6327 context_used ""
6328 6332 proof_check_time "0.000"
0 0 VernacProof "tac:yes using:no"
6531 6535 proof_build_time "0.001"
0 0 extend_shadow "0.001"
6504 6530 context_used ""
6531 6535 proof_check_time "0.000"
0 0 vo_compile_time "0.177"