diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-19 12:34:52 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-19 12:35:06 -0400 |
| commit | c1f4f952a034a4a9b8677a5b4823f97a7fab2252 (patch) | |
| tree | a4de46339986edf9d35418d90bafe29ef0fea99e /src | |
| parent | 6c026b6d1352e44e638aa1de192708e11817ecc1 (diff) | |
Fix for change in precedence of <-> vs -> in 8.4/8.5
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/Ed25519.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 2193958a3..fba6cff2d 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -286,7 +286,7 @@ Check @sign_correct Definition Fsqrt_minus1 := Eval vm_compute in ModularBaseSystem.decode (GF25519.sqrt_m1). Definition Fsqrt := PrimeFieldTheorems.F.sqrt_5mod8 Fsqrt_minus1. -Lemma bound_check_255_helper x y : (0 <= x)%Z -> BinInt.Z.to_nat x < 2^y <-> (x < 2^(Z.of_nat y))%Z. +Lemma bound_check_255_helper x y : (0 <= x)%Z -> (BinInt.Z.to_nat x < 2^y <-> (x < 2^(Z.of_nat y))%Z). Proof. intros. rewrite <-(Znat.Nat2Z.id 2) at 1. |