diff options
Diffstat (limited to 'src/Spec/ModularWordEncoding.v')
| -rw-r--r-- | src/Spec/ModularWordEncoding.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v index 7a9845e7e..5b0bdb545 100644 --- a/src/Spec/ModularWordEncoding.v +++ b/src/Spec/ModularWordEncoding.v @@ -11,7 +11,7 @@ Require Crypto.Encoding.ModularWordEncodingPre. Local Open Scope nat_scope. Section ModularWordEncoding. - Context {m : Z} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. + Context {m : positive} {sz : nat} {m_pos : (0 < m)%Z} {bound_check : Z.to_nat m < 2 ^ sz}. Definition Fm_enc (x : F m) : word sz := NToWord sz (Z.to_N (F.to_Z x)). |