COQAUX1 674cb8319be2cff2e3564b20efcaccb5 /home/allaun/SilverSight/coq/CoreFormalism/Q16_16.v
0 0 VernacProof "tac:no using:no"
164 168 proof_build_time "0.001"
0 0 le_neg2147483648_2147483647 "0.001"
159 163 context_used ""
164 168 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
226 230 proof_build_time "0.000"
0 0 le_0_2147483647 "0.000"
221 225 context_used ""
226 230 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
292 296 proof_build_time "0.000"
0 0 le_neg2147483648_0 "0.000"
287 291 context_used ""
292 296 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
373 377 proof_build_time "0.000"
0 0 le_2147483647_2147483647 "0.000"
368 372 context_used ""
373 377 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
1220 1224 proof_build_time "0.002"
0 0 clamp_bounded "0.002"
1183 1217 context_used ""
1220 1224 proof_check_time "0.001"
0 0 VernacProof "tac:no using:no"
1560 1564 proof_build_time "0.001"
0 0 clamp_idempotent "0.001"
1545 1557 context_used ""
1560 1564 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2259 2263 proof_build_time "0.000"
0 0 add_comm "0.000"
2214 2258 context_used ""
2259 2263 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2445 2449 proof_build_time "0.000"
0 0 add_in_range "0.000"
2396 2442 context_used ""
2445 2449 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2708 2712 proof_build_time "0.001"
0 0 sub_self "0.001"
2647 2705 context_used ""
2708 2712 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2818 2822 proof_build_time "0.000"
0 0 mul_comm "0.000"
2773 2817 context_used ""
2818 2822 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
2973 2977 proof_build_time "0.000"
0 0 in_range_zero "0.000"
2914 2972 context_used ""
2973 2977 proof_check_time "0.000"
0 0 VernacProof "tac:no using:no"
3127 3131 proof_build_time "0.000"
0 0 in_range_one "0.000"
3068 3126 context_used ""
3127 3131 proof_check_time "0.000"
0 0 vo_compile_time "0.140"