math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
32 stars 2 forks source link

exact_no_check for the second step of reflection #49

Closed pi8027 closed 2 years ago

pi8027 commented 2 years ago

w/o exact_no_check:

COQC theories/ops_for_b.v
Reification: 2.371427 sec.
Reflection: 83.233104 sec.
Tactic call ran for 85.808 secs (85.719u,0.084s) (success)
Reification: 0.605139 sec.
Reflection: 0.073091 sec.
Reification: 0.010927 sec.
Reflection: 0.002981 sec.
Reification: 1.228837 sec.
Reflection: 0.624552 sec.
Tactic call ran for 1.956 secs (1.956u,0.s) (success)
Reification: 18.225851 sec.
Reflection: 7.261711 sec.
Tactic call ran for 26.508 secs (26.448u,0.055s) (success)

w/ exact_no_check:

COQC theories/ops_for_b.v
Reification: 2.400271 sec.
Reflection: 82.333735 sec.
Tactic call ran for 84.949 secs (84.885u,0.06s) (success)
Reification: 0.614173 sec.
Reflection: 0.002238 sec.
Reification: 0.000897 sec.
Reflection: 0.001737 sec.
Reification: 1.225546 sec.
Reflection: 0.419238 sec.
Tactic call ran for 1.775 secs (1.775u,0.s) (success)
Reification: 18.276137 sec.
Reflection: 4.385671 sec.
Tactic call ran for 23.685 secs (23.647u,0.035s) (success)