aboutsummaryrefslogtreecommitdiff
path: root/src/ModularArithmetic/ModularBaseSystemOpt.v
diff options
context:
space:
mode:
authorGravatar jadep <jade.philipoom@gmail.com>2016-07-20 17:08:00 -0400
committerGravatar jadep <jade.philipoom@gmail.com>2016-07-20 17:08:00 -0400
commit55e6291f60ff65fa484a7bad1806adcf4be78cf1 (patch)
tree921358486cbc65abcd80d08fa858f29a6cbc6e3b /src/ModularArithmetic/ModularBaseSystemOpt.v
parent4ea92779f54a7f6a49e334cd6071096be57c40ca (diff)
parent4fbf246cb392496e676e314c11bc2962d37caad7 (diff)
merge
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
-rw-r--r--src/ModularArithmetic/ModularBaseSystemOpt.v4
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.