Make [base] and [log_cap] notations

Also use [ZUtil.Z.pow2_mod].  This lets us remove the dependency of
ModularBaseSystem on ModularArithmetic.PseudoMersenneBaseParamProofs.

This is a small part of reorganizing and factoring ModularBaseSystem for
use with Barrett reduction.

1 files changed, 3 insertions, 4 deletions

diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v
index 847967f52..7d0495ef3 100644
--- a/src/ModularArithmetic/Pow2Base.v
+++ b/src/ModularArithmetic/Pow2Base.v
@@ -14,14 +14,13 @@ Section Pow2Base.
     | w :: lw => 1 :: map (Z.mul (two_p w)) (base_from_limb_widths lw)
     end.
 
-  Local Notation "{base}" := (base_from_limb_widths limb_widths).
-
+  Local Notation base := (base_from_limb_widths limb_widths).
 
   Definition bounded us := forall i, 0 <= nth_default 0 us i < 2 ^ w[i].
 
   Definition upper_bound := 2 ^ (sum_firstn limb_widths (length limb_widths)).
 
-  Fixpoint decode_bitwise' us i acc := 
+  Fixpoint decode_bitwise' us i acc :=
     match i with
     | O => acc
     | S i' => decode_bitwise' us i' (Z.lor (nth_default 0 us i') (Z.shiftl acc w[i']))
@@ -40,4 +39,4 @@ Section Pow2Base.
   (* max must be greater than input; this is used to truncate last digit *)
   Definition encodeZ x:= encode' x (length limb_widths).
 
-End Pow2Base.
\ No newline at end of file
+End Pow2Base.