diff options
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemList.v | 4 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 6 |
2 files changed, 5 insertions, 5 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. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index a1370d33e..d740cca17 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -208,7 +208,7 @@ Section PseudoMersenneProofs. split; [ intuition | ]. destruct Hcarry_done as [Hnth_nonneg Hshiftr_0]. apply Z.shiftr_eq_0_iff in Hshiftr_0. - destruct Hshiftr_0 as [nth_0 | []]; [ rewrite nth_0; zero_bounds | ]. + destruct Hshiftr_0 as [nth_0 | [] ]; [ rewrite nth_0; zero_bounds | ]. apply Z.log2_lt_pow2; auto. - rewrite nth_default_out_of_bounds by omega. split; zero_bounds. @@ -482,8 +482,8 @@ Section CanonicalizationProofs. Qed. Hint Rewrite @nth_default_carry using (omega || distr_length; omega) : push_nth_default. - Local Notation "u '[' i ']' " := (nth_default 0 u i) (at level 30). - Local Notation "u '{{' i '}}' " := (carry_sequence (make_chain i) u) (at level 30). + Local Notation "u [ i ]" := (nth_default 0 u i). + Local Notation "u {{ i }}" := (carry_sequence (make_chain i) u) (at level 30). (* Can't rely on [Reserved Notation]: https://coq.inria.fr/bugs/show_bug.cgi?id=4970 *) Lemma bound_during_first_loop : forall i n us, length us = length limb_widths -> |