diff options
Diffstat (limited to 'src/Arithmetic/Saturated/MontgomeryAPI.v')
| -rw-r--r-- | src/Arithmetic/Saturated/MontgomeryAPI.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v index 5b5ec1748..6dee1d22b 100644 --- a/src/Arithmetic/Saturated/MontgomeryAPI.v +++ b/src/Arithmetic/Saturated/MontgomeryAPI.v @@ -395,7 +395,7 @@ Section API. eapply small_left_append; eauto. rewrite @B.Positional.sat_add_div by omega. repeat match goal with H:_|-_=> unique pose proof (eval_small _ _ H) end. - cbv [eval] in *; Z.div_mod_to_quot_rem; nia. + cbv [eval] in *; Z.div_mod_to_quot_rem_in_goal; nia. Qed. Lemma small_join0 {n} b : small b -> small (@join0 n b). |