diff options
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemList.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemList.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v index b46429fcc..c556427b9 100644 --- a/src/ModularArithmetic/ModularBaseSystemList.v +++ b/src/ModularArithmetic/ModularBaseSystemList.v @@ -14,7 +14,7 @@ Local Open Scope Z_scope. Section Defs. Context `{prm :PseudoMersenneBaseParams} (modulus_multiple : digits). Local Notation base := (base_from_limb_widths limb_widths). - Local Notation "u [ i ]" := (nth_default 0 u i) (at level 40). + Local Notation "u [ i ]" := (nth_default 0 u i). Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us). @@ -68,4 +68,4 @@ Section Defs. Otherwise, it's all zeroes, and the subtractions do nothing. *) map2 (fun x y => x - y) us (map (Z.land and_term) modulus_digits). -End Defs.
\ No newline at end of file +End Defs. |