diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-12 14:26:52 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-12 14:26:59 -0500 |
| commit | 86ebe2d8218eb5d3559a3c17cbd2652636d4d564 (patch) | |
| tree | a5ed7a8c1a43ce898dbc08f028a4b9233cf62b69 /src/Specific | |
| parent | 070b8b05a1d294eaf7f283bbe0cf08e85df33a93 (diff) | |
More 8.4pl2 fixes
Also, I meant 8.4pl2 in the previous commit, not 8.2
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF25519Bounded.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v index 92ecf174a..d79e413a4 100644 --- a/src/Specific/GF25519Bounded.v +++ b/src/Specific/GF25519Bounded.v @@ -190,7 +190,7 @@ Proof. end; try solve [ (apply Z.log2_lt_pow2_alt; [ vm_compute; reflexivity | ]); - eapply Z.le_lt_trans; try apply Z.land_upper_bound_r; try apply neg_range; instantiate; try (vm_compute; discriminate); reflexivity]; + eapply Z.le_lt_trans; try apply Z.land_upper_bound_r; try apply neg_range; instantiate; try match goal with |- ?G => not has_evar G; vm_compute; discriminate end; reflexivity]; try match goal with | |- 0 <= _ - _ => lower_bound_minus_ge_modulus | |- Z.log2 (_ - _) < _ => upper_bound_minus_ge_modulus |