diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/IntegrationTest.v | 2 | ||||
| -rw-r--r-- | src/Util/BoundedWord.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/Specific/IntegrationTest.v b/src/Specific/IntegrationTest.v index 49fb55969..e37dacdb7 100644 --- a/src/Specific/IntegrationTest.v +++ b/src/Specific/IntegrationTest.v @@ -7,7 +7,7 @@ Require Import Crypto.NewBaseSystem. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Specific.NewBaseSystemTest. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. +Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. Import ListNotations. Section BoundedField25p5. diff --git a/src/Util/BoundedWord.v b/src/Util/BoundedWord.v index cfd27a231..e5c3720fe 100644 --- a/src/Util/BoundedWord.v +++ b/src/Util/BoundedWord.v @@ -5,8 +5,8 @@ Require Import Crypto.Util.FixedWordSizes. Definition BoundedWord n (bitwidth : nat) (bounds : tuple zrange n) : Type := - { x : tuple (wordT bitwidth) n - | is_bounded_by (Some (Z.of_nat bitwidth)) bounds + { x : tuple (wordT (Nat.log2 bitwidth)) n + | is_bounded_by None bounds (map wordToZ x)}. Definition BoundedWordToZ n w b (BW :BoundedWord n w b) |