diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-19 14:50:50 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-19 14:50:50 -0700 |
| commit | 70f3ef2ad457248aeb361c68af25a74169e0e861 (patch) | |
| tree | fca19e5de83065145555ad42828e3a3d4c7b3df4 /src/ModularArithmetic | |
| parent | cdd44cf2718255b699ce6e77cfd4333a736ee804 (diff) | |
Fix side-condition from previous commit
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/Pow2BaseProofs.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 45fea0356..ca28896dd 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -788,7 +788,8 @@ Section carrying. Hint Rewrite @nth_default_carry_simple using (omega || distr_length; omega) : push_nth_default. End carrying. -Hint Rewrite @length_carry_gen @base_from_limb_widths_length : distr_length. +Hint Rewrite @length_carry_gen : distr_length. Hint Rewrite @length_carry_simple @length_carry_simple_sequence @length_make_chain @length_full_carry_chain @length_carry_simple_full : distr_length. Hint Rewrite @nth_default_carry_simple_full @nth_default_carry_gen_full : push_nth_default. Hint Rewrite @nth_default_carry_simple @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. +Hint Rewrite @base_from_limb_widths_length using auto with nocore distr_length : distr_length. |