diff options
author | 2016-10-19 20:26:07 -0400 | |
---|---|---|
committer | 2016-10-19 20:26:07 -0400 | |
commit | 827d9aa160aa9d1fc92ace087915604d667e5502 (patch) | |
tree | 91c6684103c706d67aa1aca5c9ea9521cdcb8a74 | |
parent | ce564c5015e1868adf1d8353115931701b8273a6 (diff) |
Removed the lingering TODO and print statement that @JasonGross helpfully pointed out
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519.v | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 50da3a683..f8ad0969d 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -508,7 +508,6 @@ Section CarryProofs. reflexivity. Qed. - Print carry_opp. Lemma carry_opp_rep : forall coeff coeff_mod a, eq (carry_opp carry_chain coeff coeff_mod a) 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). |