made BaseVector instance global

6 files changed, 4 insertions, 7 deletions

diff --git a/src/BaseSystem.v b/src/BaseSystem.v
index f3a1a0fdb..627550440 100644
--- a/src/BaseSystem.v
+++ b/src/BaseSystem.v
@@ -85,6 +85,7 @@ Section BaseSystem.
 
 End BaseSystem.
 
+(* Example : polynomial base system *)
 Section PolynomialBaseCoefs.
   Context (b1 : positive) (baseLength : nat) (baseLengthNonzero : NPeano.ltb 0 baseLength = true).
   (** PolynomialBaseCoefs generates base vectors for [BaseSystem]. *)
diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v
index 746791d8d..2e65df9bd 100644
--- a/src/ModularArithmetic/ExtendedBaseVector.v
+++ b/src/ModularArithmetic/ExtendedBaseVector.v
@@ -9,7 +9,6 @@ Local Open Scope Z_scope.
 
 Section ExtendedBaseVector.
   Context `{prm : PseudoMersenneBaseParams}.
-  Existing Instance bv.
 
   (* This section defines a new BaseVector that has double the length of the BaseVector
   * used to construct [params]. The coefficients of the new vector are as follows:
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index d121e9d5c..2bfcdcf0b 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -7,7 +7,6 @@ Local Open Scope Z_scope.
 
 Section PseudoMersenneBase.
   Context `{prm :PseudoMersenneBaseParams}.
-  Existing Instance bv.
   
   Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us).
   
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 524c2da27..7efccbade 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -9,7 +9,6 @@ Local Open Scope Z_scope.
 
 Section PseudoMersenneProofs.
   Context `{prm :PseudoMersenneBaseParams}.
-  Existing Instance bv.
 
   Local Hint Unfold decode.
   Local Notation "u '~=' x" := (rep u x) (at level 70).
@@ -251,7 +250,6 @@ End PseudoMersenneProofs.
 
 Section CarryProofs.
   Context `{prm : PseudoMersenneBaseParams}.
-  Existing Instance bv.
   Local Notation "u '~=' x" := (rep u x) (at level 70).
   Hint Unfold log_cap.
   
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 847b8e85f..93e6bc1f0 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -268,7 +268,7 @@ Section PseudoMersenneBaseParamProofs.
      rewrite <- base_length; assumption.
    Qed.
 
-  Instance bv : BaseSystem.BaseVector base := {
+  Global Instance bv : BaseSystem.BaseVector base := {
     base_positive := base_positive;
     b0_1 := b0_1;
     base_good := base_good
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParams.v b/src/ModularArithmetic/PseudoMersenneBaseParams.v
index 122cac0ab..09f4bc68e 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParams.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParams.v
@@ -14,6 +14,7 @@ Class PseudoMersenneBaseParams (modulus : Z) := {
     sum_firstn limb_widths i + sum_firstn limb_widths j;
   k : Z;
   c : Z;
+  k_matches_limb_widths : sum_firstn limb_widths (length limb_widths) = k;
   modulus_pseudomersenne : modulus = 2^k - c;
   prime_modulus : Znumtheory.prime modulus;
   limb_widths_match_modulus : forall i j,
@@ -21,6 +22,5 @@ Class PseudoMersenneBaseParams (modulus : Z) := {
     (j < length limb_widths)%nat ->
     (i + j >= length limb_widths)%nat ->
     let w_sum := sum_firstn limb_widths in
-    k + w_sum (i + j - length limb_widths)%nat <= w_sum i + w_sum j;
-  k_matches_limb_widths : sum_firstn limb_widths (length limb_widths) = k
+    k + w_sum (i + j - length limb_widths)%nat <= w_sum i + w_sum j
 }.