diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-11 16:26:04 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-11 16:26:04 -0400 |
| commit | 3f83ec83817da219c79ae6d65825d861c28847df (patch) | |
| tree | aec81a7ec6d5d1bf4c7d24116866e018575d2836 | |
| parent | 3170c524a121c8d56a88eadabe6f7cdae53d4871 (diff) | |
Tweaks for 8.4 compatibility
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 4 | ||||
| -rw-r--r-- | src/Testbit.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 0e29cf0c0..50083e275 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -325,7 +325,7 @@ Section Pow2BaseProofs. | |- _ => rewrite nth_default_base | |- _ => rewrite IHi | |- _ => rewrite <-Z.lor_shiftl by (rewrite ?Z.pow2_mod_spec; try apply Z.mod_pos_bound; zero_bounds) - | |- appcontext[Nat.min ?x ?y] => (rewrite Nat.min_l by omega || rewrite Nat.min_r by omega) + | |- appcontext[min ?x ?y] => (rewrite Nat.min_l by omega || rewrite Nat.min_r by omega) | |- appcontext[2 ^ ?a * _] => rewrite (Z.mul_comm (2 ^ a)); rewrite <-Z.shiftl_mul_pow2 | |- _ => solve [auto] | |- _ => lia @@ -343,6 +343,7 @@ Section Pow2BaseProofs. | |- _ => rewrite sum_firstn_succ_default in *; pose proof (nth_default_limb_widths_nonneg i); omega end. + Qed. Lemma testbit_decode_firstn_high : forall us i n, @@ -862,7 +863,6 @@ Section TestbitDecode. End TestbitDecode. - Section carrying_helper. Context {limb_widths} (limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w). Local Notation base := (base_from_limb_widths limb_widths). diff --git a/src/Testbit.v b/src/Testbit.v index bed2f5a0f..6bc693fae 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -46,7 +46,7 @@ Section Testbit. | |- _ => rewrite nth_default_out_of_bounds by omega | |- _ => rewrite nth_default_uniform_base by omega | |- false = Z.testbit (decode _ _) _ => rewrite testbit_decode_high - | |- _ => rewrite sum_firstn_uniform_base by (eassumption || omega) + | |- _ => rewrite (@sum_firstn_uniform_base width) by (eassumption || omega) | |- _ => rewrite sum_firstn_succ_default | |- Z.testbit (nth_default _ _ ?x) _ = Z.testbit (decode _ _) _ => destruct (lt_dec x (length limb_widths)); |