diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-06 13:48:40 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-06 13:48:40 -0400 |
| commit | cc920cf2a3aa859a93e8e990a19a960f78cd3b1b (patch) | |
| tree | ed93d93f82578239ef2e0a6843e52e1d6968a5ef /src/ModularArithmetic/ModularBaseSystemOpt.v | |
| parent | 260b20cab885deae59a305492567dc0f0d88b3a8 (diff) | |
| parent | 0cea3e2f80408a25954f820faebf5cd79d2e13ae (diff) | |
Merged changes, including new ZUtil conventions.
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemOpt.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index bb9b1674e..ce11b157b 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -22,7 +22,7 @@ Definition Z_div_opt := Eval compute in Z.div. Definition Z_pow_opt := Eval compute in Z.pow. Definition Z_opp_opt := Eval compute in Z.opp. Definition Z_shiftl_opt := Eval compute in Z.shiftl. -Definition Z_shiftl_by_opt := Eval compute in Z_shiftl_by. +Definition Z_shiftl_by_opt := Eval compute in Z.shiftl_by. Definition nth_default_opt {A} := Eval compute in @nth_default A. Definition set_nth_opt {A} := Eval compute in @set_nth A. @@ -502,11 +502,11 @@ Section Multiplication. cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros ext_base reduce]. rewrite <- mul'_opt_correct. change @base with base_opt. - rewrite map_shiftl by apply k_nonneg. + rewrite Z.map_shiftl by apply k_nonneg. rewrite c_subst. rewrite k_subst. change @map with @map_opt. - change @Z_shiftl_by with @Z_shiftl_by_opt. + change @Z.shiftl_by with @Z_shiftl_by_opt. reflexivity. Defined. @@ -671,4 +671,4 @@ Section Canonicalization. auto using freeze_opt_preserves_rep. Qed. -End Canonicalization.
\ No newline at end of file +End Canonicalization. |