ported IterAssocOp to use monoid rather than a billion context variables that add up to a monoid

1 files changed, 1 insertions, 1 deletions

diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 8e526745c..951f848bf 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -220,7 +220,7 @@ Section FandZ.
     reflexivity.
   Qed.
 
-  Lemma pow_nat_iter_op_correct: forall (x:F m) n, (nat_iter_op mul 1) (N.to_nat n) x = x^n.
+  Lemma pow_nat_iter_op_correct: forall (x:F m) n, (@nat_iter_op _ mul 1) (N.to_nat n) x = x^n.
   Proof.
     induction n using N.peano_ind;
       destruct (F_pow_spec x) as [pow_0 pow_succ];