aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic
diff options
context:
space:
mode:
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r--src/ModularArithmetic/ModularBaseSystemProofs.v1
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)