diff options
Diffstat (limited to 'src/Util/ZUtil/Tactics/RewriteModSmall.v')
| -rw-r--r-- | src/Util/ZUtil/Tactics/RewriteModSmall.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Tactics/RewriteModSmall.v b/src/Util/ZUtil/Tactics/RewriteModSmall.v index 45598b0c5..6b3b05a41 100644 --- a/src/Util/ZUtil/Tactics/RewriteModSmall.v +++ b/src/Util/ZUtil/Tactics/RewriteModSmall.v @@ -20,7 +20,7 @@ Module Z. | [ H : context[(_ mod _)%Z] |- _ ] => revert H end. - Z.div_mod_to_quot_rem. + Z.div_mod_to_quot_rem_in_goal. lazymatch goal with | [ H : a = (?x * ?n * ?q) + _, H' : a = (?n * ?q') + _ |- _ ] => assert (q' = x * q) by nia; subst q'; nia |