diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-11 14:16:34 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2016-11-11 14:45:17 -0500 |
| commit | 1ce3512d0e1b6761868b1c6234424cbb82a65d22 (patch) | |
| tree | d3baa644536ea89bad1e3aeef42d0471dd38671f /src | |
| parent | 9c8f8c4e1457ca328df1c3013c59ea43adb8c410 (diff) | |
Fix proofs broken by stronger preconditions
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 90cac35e2..3d10af14d 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -1218,7 +1218,7 @@ Proof. assert (i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4 \/ i = 5 \/ i = 6 \/ i = 7) by omega. repeat match goal with H : (_ \/ _)%type |- _ => destruct H; subst end; cbv [nth_default nth_error value]; try (apply pow2_mod_range; omega). - repeat apply shiftr_range; apply WordNZ_range_mono; cbv; + repeat apply shiftr_range; try omega; apply WordNZ_range_mono; cbv; congruence. } { rewrite !nth_default_out_of_bounds by (rewrite ?Tuple.length_to_list; cbv [length]; omega). |