diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-12 14:25:57 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-12 14:25:57 -0500 |
| commit | 070b8b05a1d294eaf7f283bbe0cf08e85df33a93 (patch) | |
| tree | a460b9c72da567bd362087d47f3ee2ea1476cca8 /src/Specific | |
| parent | edac504b9f30c07e752719b616fe8730b88ff36c (diff) | |
Fix for Coq 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 5f2adc9c9..92ecf174a 100644 --- a/src/Specific/GF25519Bounded.v +++ b/src/Specific/GF25519Bounded.v @@ -170,7 +170,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]; match goal with | |- 0 <= _ - _ => lower_bound_minus_ge_modulus | |- Z.log2 (_ - _) < _ => upper_bound_minus_ge_modulus |