diff options
Diffstat (limited to 'src/Arithmetic/Saturated/Freeze.v')
| -rw-r--r-- | src/Arithmetic/Saturated/Freeze.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Arithmetic/Saturated/Freeze.v b/src/Arithmetic/Saturated/Freeze.v index b56a69a3d..658eb867d 100644 --- a/src/Arithmetic/Saturated/Freeze.v +++ b/src/Arithmetic/Saturated/Freeze.v @@ -102,6 +102,7 @@ Section Freeze. pose proof Z.add_get_carry_full_mod. pose proof Z.add_get_carry_full_div. pose proof div_correct. pose proof modulo_correct. + pose proof @div_id. pose proof @modulo_id. pose proof @Z.add_get_carry_full_cps_correct. autorewrite with uncps push_id push_basesystem_eval. |