use [positive] for [F] modulus, char_ge_C instead of char_gt_C

1 files changed, 3 insertions, 3 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 3b0231191..34a331fa1 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -30,12 +30,12 @@ Class CarryChain (limb_widths : list Z) :=
     carry_chain_valid : forall i, In i carry_chain -> (i < length limb_widths)%nat
   }.
 
-  Class SubtractionCoefficient {m : Z} {prm : PseudoMersenneBaseParams m} := {
+  Class SubtractionCoefficient {m : positive} {prm : PseudoMersenneBaseParams m} := {
     coeff : tuple Z (length limb_widths);
     coeff_mod: decode coeff = 0%F
   }.
 
-  Class ExponentiationChain {m : Z} {prm : PseudoMersenneBaseParams m} (exp : Z) := {
+  Class ExponentiationChain {m : positive} {prm : PseudoMersenneBaseParams m} (exp : Z) := {
     chain : list (nat * nat);
     chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N exp
   }.
@@ -85,7 +85,7 @@ Section FieldOperationProofs.
     + apply F.of_Z_to_Z.
     + apply bv.
     + rewrite <-F.mod_to_Z.
-      match goal with |- appcontext [?a mod modulus] =>
+      match goal with |- appcontext [?a mod (Z.pos modulus)] =>
                       pose proof (Z.mod_pos_bound a modulus modulus_pos) end.
       pose proof lt_modulus_2k.
       omega.