diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-10 16:02:35 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-10 16:02:35 -0400 |
| commit | dacd72b5151bc01a4e35d2290f0aab9aca32cb6d (patch) | |
| tree | 14adfa5fd032b688aded5905aa6f4d3f3e8da2ea /src/Util/ZUtil | |
| parent | 1d3a90c2fb96ad5704718e9c0eb214ca177b04f8 (diff) | |
Fix a typo
Diffstat (limited to 'src/Util/ZUtil')
| -rw-r--r-- | src/Util/ZUtil/EquivModulo.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil/EquivModulo.v b/src/Util/ZUtil/EquivModulo.v index 586d16828..3ca8c60c5 100644 --- a/src/Util/ZUtil/EquivModulo.v +++ b/src/Util/ZUtil/EquivModulo.v @@ -32,7 +32,7 @@ Module Z. Local Instance pow_mod_Proper : Proper (equiv_modulo ==> eq ==> equiv_modulo) Z.pow. Proof. intros ?? H ???; subst; hnf in H |- *. - rewrite Z.mod_pow_full, H, <- Z.power_mod_full; reflexivity. + rewrite Z.mod_pow_full, H, <- Z.mod_pow_full; reflexivity. Qed. Local Instance modulo_equiv_modulo_Proper |