diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-10 21:00:33 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2016-11-11 16:07:28 -0500 |
| commit | 790e9ccfc164241e32d6fe4ba80c85e17cbb7051 (patch) | |
| tree | 61730ffc9ffc0e06e8315183e41f4d3734ad063e /src | |
| parent | 4d6d788ff04ec7b08d522099b6841fd16d6fae5c (diff) | |
Remove 8.6 only syntax
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/GF25519BoundedCommon.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index 4f0c9b4de..d006e58af 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -692,7 +692,7 @@ Notation iunop_WireToFE_correct_and_bounded irop op (** TODO(andreser): Remove me in favor of a GF25519.v definition *) Definition prefreeze := -fun '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) => +fun fs => let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := fs in dlet a := f9 in dlet a0 := (Z.shiftr a 26 + f8)%Z in dlet a1 := (Z.shiftr a0 25 + f7)%Z in |