From 827d9aa160aa9d1fc92ace087915604d667e5502 Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 19 Oct 2016 20:26:07 -0400 Subject: Removed the lingering TODO and print statement that @JasonGross helpfully pointed out --- src/ModularArithmetic/ModularBaseSystemProofs.v | 1 - 1 file changed, 1 deletion(-) (limited to 'src/ModularArithmetic') 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) -- cgit v1.2.3