diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-02-15 13:18:40 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | 0a6e65e3cec0a8f00f357d82489532203f315389 (patch) | |
| tree | b7bc706ce46b38e3c43f9375fd5a2dd9859d056a /src/Spec/CompleteEdwardsCurve.v | |
| parent | 0a9ea9df752b078bbd89f765cf760081036bd51a (diff) | |
address some code review comments
Diffstat (limited to 'src/Spec/CompleteEdwardsCurve.v')
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index 05f61f159..770a2d02d 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -20,7 +20,7 @@ Module E. Context {a d: F}. Class twisted_edwards_params := { - char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul BinNat.N.two; + char_gt_2 : @Ring.char_gt F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.one); nonzero_a : a <> 0; square_a : exists sqrt_a, sqrt_a^2 = a; nonsquare_d : forall x, x^2 <> d |