diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-19 20:26:07 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-19 20:26:07 -0400 |
| commit | 827d9aa160aa9d1fc92ace087915604d667e5502 (patch) | |
| tree | 91c6684103c706d67aa1aca5c9ea9521cdcb8a74 /src/Specific/GF25519.v | |
| parent | ce564c5015e1868adf1d8353115931701b8273a6 (diff) | |
Removed the lingering TODO and print statement that @JasonGross helpfully pointed out
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 46de0cbec..36feb2f4c 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -406,7 +406,6 @@ Proof. Qed. -(** TODO(jadep from jgross): Fill me in *) Lemma carry_field25519 : @field fe25519 eq zero_ one_ carry_opp carry_add carry_sub mul inv div. Proof. pose proof (Equivalence_Reflexive : Reflexive eq). |