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/ModularArithmetic | |
| parent | ce564c5015e1868adf1d8353115931701b8273a6 (diff) | |
Removed the lingering TODO and print statement that @JasonGross helpfully pointed out
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 1 |
1 files changed, 0 insertions, 1 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) |