From 70f3ef2ad457248aeb361c68af25a74169e0e861 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 14:50:50 -0700 Subject: Fix side-condition from previous commit --- src/ModularArithmetic/Pow2BaseProofs.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/ModularArithmetic') 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. -- cgit v1.2.3