diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-22 21:35:47 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-22 21:35:47 -0400 |
| commit | ff040390affcd3a1fdfbddb5301e5ecb47ceeff6 (patch) | |
| tree | c2287843a07457b55f80214d18687a36e8bfc314 /src/Util/ZUtil | |
| parent | f79880fc1f986c7b46a185c90a70233fef9698fb (diff) | |
Fix a typo in push_Zmod that was causing looping
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/Modulo/PullPush.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/Modulo/PullPush.v b/src/Util/ZUtil/Modulo/PullPush.v index 7e3a9b46a..a284e61c9 100644 --- a/src/Util/ZUtil/Modulo/PullPush.v +++ b/src/Util/ZUtil/Modulo/PullPush.v @@ -127,5 +127,5 @@ Module Z. Lemma opp_mod_mod_push a n : NoZMod a -> (-a) mod n = (-(a mod n)) mod n. Proof. intros; apply opp_mod_mod; assumption. Qed. - Hint Rewrite opp_mod_mod using solve [ NoZMod ] : push_Zmod. + Hint Rewrite opp_mod_mod_push using solve [ NoZMod ] : push_Zmod. End Z. |