diff options
author | jadep <jade.philipoom@gmail.com> | 2016-07-20 17:08:00 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-07-20 17:08:00 -0400 |
commit | 55e6291f60ff65fa484a7bad1806adcf4be78cf1 (patch) | |
tree | 921358486cbc65abcd80d08fa858f29a6cbc6e3b /src/ModularArithmetic/ModularBaseSystemOpt.v | |
parent | 4ea92779f54a7f6a49e334cd6071096be57c40ca (diff) | |
parent | 4fbf246cb392496e676e314c11bc2962d37caad7 (diff) |
merge
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index c4d4ccca0..d1a6f6228 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -494,12 +494,12 @@ Section Multiplication. rewrite <- from_list_default_eq with (d := 0%Z). change (@from_list_default Z) with (@from_list_default_opt Z). apply f_equal. - rewrite ext_base_alt. + rewrite ext_base_alt by auto using limb_widths_pos with zarith. rewrite <- mul'_opt_correct. change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. rewrite Z.map_shiftl by apply k_nonneg. rewrite c_subst. - rewrite k_subst. + fold k; rewrite k_subst. change @map with @map_opt. change @Z.shiftl_by with @Z_shiftl_by_opt. reflexivity. |