diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-26 10:01:18 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-06-26 10:02:10 -0400 |
| commit | cac291e09c4f1a945959d3306dd62d030cbc7ac3 (patch) | |
| tree | 46c1e2c573071824860edcf465d09e570d25dbb6 /src/Specific/MontgomeryP256_128.v | |
| parent | 3794a3b93f8aee88f4daf75ba3dd09eabc25e857 (diff) | |
More proof fixing
Diffstat (limited to 'src/Specific/MontgomeryP256_128.v')
| -rw-r--r-- | src/Specific/MontgomeryP256_128.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v index 26ad676b8..086a454e8 100644 --- a/src/Specific/MontgomeryP256_128.v +++ b/src/Specific/MontgomeryP256_128.v @@ -311,7 +311,7 @@ Definition nonzero : { f:Tuple.tuple Z sz -> Z Proof. exists (proj1_sig nonzero'). abstract ( - intros eval A H **; rewrite (proj2_sig nonzero'), eval_nonzero by eassumption; + intros eval A H **; rewrite (proj2_sig nonzero'), (@eval_nonzero r) by (eassumption || reflexivity); subst eval; unfold montgomery_to_F, Saturated.uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul; rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; |