From ecf3e0f6ae2cf7267956fd5c2fe52a56d043f465 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Tue, 19 Jul 2016 15:01:21 -0700
Subject: {base} -> base

---
 src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 16 ++++++++--------
 src/Testbit.v                                         |  8 ++++----
 2 files changed, 12 insertions(+), 12 deletions(-)

(limited to 'src')

diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 07114b1e4..1cb87910d 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -11,7 +11,7 @@ Local Open Scope Z_scope.
 
 Section PseudoMersenneBaseParamProofs.
   Context `{prm : PseudoMersenneBaseParams}.
-  Local Notation "{base}" := (base_from_limb_widths limb_widths).
+  Local Notation base := (base_from_limb_widths limb_widths).
 
   Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w.
   Proof.
@@ -35,9 +35,9 @@ Section PseudoMersenneBaseParamProofs.
     (i   <  length limb_widths)%nat ->
     (j   <  length limb_widths)%nat ->
     (i+j >= length limb_widths)%nat->
-    let b := nth_default 0 {base} in
-    let r := (b i * b j)  /   (2^k * b (i+j-length {base})%nat) in
-              b i * b j = r * (2^k * b (i+j-length {base})%nat).
+    let b := nth_default 0 base in
+    let r := (b i * b j)  /   (2^k * b (i+j-length base)%nat) in
+              b i * b j = r * (2^k * b (i+j-length base)%nat).
   Proof.
     intros.
     rewrite (Z.mul_comm r).
@@ -59,8 +59,8 @@ Section PseudoMersenneBaseParamProofs.
   Qed.
 
    Lemma base_good : forall i j : nat,
-                (i + j < length {base})%nat ->
-                let b := nth_default 0 {base} in
+                (i + j < length base)%nat ->
+                let b := nth_default 0 base in
                 let r := b i * b j / b (i + j)%nat in
                 b i * b j = r * b (i + j)%nat.
    Proof.
@@ -76,12 +76,12 @@ Section PseudoMersenneBaseParamProofs.
      rewrite <-base_from_limb_widths_length; auto using limb_widths_nonneg.
    Qed.
 
-  Lemma base_length : length {base} = length limb_widths.
+  Lemma base_length : length base = length limb_widths.
   Proof.
     auto using base_from_limb_widths_length.
   Qed.
 
-  Global Instance bv : BaseSystem.BaseVector {base} := {
+  Global Instance bv : BaseSystem.BaseVector base := {
     base_positive := base_positive limb_widths_nonneg;
     b0_1 := fun x => b0_1 x limb_widths_nonnil;
     base_good := base_good
diff --git a/src/Testbit.v b/src/Testbit.v
index 13d56f207..8a9b12c61 100644
--- a/src/Testbit.v
+++ b/src/Testbit.v
@@ -13,7 +13,7 @@ Section Testbit.
   Context {width : Z} (limb_width_pos : 0 < width).
   Context (limb_widths : list Z) (limb_widths_nonnil : limb_widths <> nil)
     (limb_widths_uniform : forall w, In w limb_widths -> w = width).
-  Local Notation "{base}" := (base_from_limb_widths limb_widths).
+  Local Notation base := (base_from_limb_widths limb_widths).
 
   Definition testbit (us : list Z) (n : nat) :=
     Z.testbit (nth_default 0 us (n / (Z.to_nat width))) (Z.of_nat (n mod Z.to_nat width)%nat).
@@ -22,7 +22,7 @@ Section Testbit.
 
   Lemma testbit_spec' : forall a b us, (0 <= b < width) ->
     bounded limb_widths us -> (length us <= length limb_widths)%nat ->
-    Z.testbit (nth_default 0 us a) b = Z.testbit (decode {base} us) (Z.of_nat a * width + b).
+    Z.testbit (nth_default 0 us a) b = Z.testbit (decode base us) (Z.of_nat a * width + b).
   Proof.
     induction a; destruct us; intros;
       match goal with H : bounded _ _ |- _ =>
@@ -42,7 +42,7 @@ Section Testbit.
 
   Lemma testbit_spec : forall n us, (length us = length limb_widths)%nat ->
     bounded limb_widths us ->
-    testbit us n = Z.testbit (BaseSystem.decode {base} us) (Z.of_nat n).
+    testbit us n = Z.testbit (BaseSystem.decode base us) (Z.of_nat n).
   Proof.
     cbv [testbit]; intros.
     pose proof limb_width_pos as limb_width_pos_nat.
@@ -54,4 +54,4 @@ Section Testbit.
     rewrite Nat2Z.inj_add, Nat2Z.inj_mul, Z2Nat.id; ring || omega.
   Qed.
 
-End Testbit.
\ No newline at end of file
+End Testbit.
-- 
cgit v1.2.3