diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-02 00:01:35 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-06-05 18:47:35 -0400 |
| commit | 7488682db4cf259e0bb0c886e13301c32a2eeaa2 (patch) | |
| tree | 9baf80699c9f00b01d3180504d58351b6ecc0f33 /src/Util/ZUtil/Testbit.v | |
| parent | c4a0d1fdde22dbd2faaa1753e973ee9602076ee8 (diff) | |
Don't rely on autogenerated names
This fixes all of the private-names warnings emitted by
compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus
the ones in coqprime, which I didn't touch).
Diffstat (limited to 'src/Util/ZUtil/Testbit.v')
| -rw-r--r-- | src/Util/ZUtil/Testbit.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Util/ZUtil/Testbit.v b/src/Util/ZUtil/Testbit.v index a315f7e4b..175d07b02 100644 --- a/src/Util/ZUtil/Testbit.v +++ b/src/Util/ZUtil/Testbit.v @@ -22,7 +22,7 @@ Module Z. then true else if Z_lt_dec m n then true else false. Proof. - intros. + intros n m. repeat (break_match || autorewrite with Ztestbit); try reflexivity; try omega. unfold Z.ones. rewrite <- Z.shiftr_opp_r, Z.shiftr_eq_0 by (simpl; omega); simpl. @@ -34,7 +34,7 @@ Module Z. Lemma testbit_pow2_mod : forall a n i, 0 <= n -> Z.testbit (Z.pow2_mod a n) i = if Z_lt_dec i n then Z.testbit a i else false. Proof. - cbv [Z.pow2_mod]; intros; destruct (Z_le_dec 0 i); + cbv [Z.pow2_mod]; intros a n i H; destruct (Z_le_dec 0 i); repeat match goal with | |- _ => rewrite Z.testbit_neg_r by omega | |- _ => break_innermost_match_step @@ -50,7 +50,7 @@ Module Z. then if Z_lt_dec i 0 then false else Z.testbit a i else if Z_lt_dec i n then Z.testbit a i else false. Proof. - intros; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ]. + intros a n i; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ]. unfold Z.pow2_mod. autorewrite with Ztestbit_full; repeat break_match; @@ -80,7 +80,7 @@ Module Z. Lemma testbit_add_shiftl_low : forall i, (0 <= i) -> forall a b n, (i < n) -> Z.testbit (a + Z.shiftl b n) i = Z.testbit a i. Proof. - intros. + intros i H a b n H0. erewrite Z.testbit_low; eauto. rewrite Z.land_ones, Z.shiftl_mul_pow2 by omega. rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 n); omega). |