diff options
| -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). |