diff options
| -rw-r--r-- | contrib/ring/Ring_normalize.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 2590dd72bc..536d2d3034 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -602,7 +602,7 @@ Rewrite H. Rewrite varlist_merge_ok. Repeat Rewrite (SR_distr_right T). Repeat Rewrite <- (SR_mult_assoc T). -Repeat Rewrite <- (SR_pus_assoc T). +Repeat Rewrite <- (SR_plus_assoc T). Rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). Reflexivity. @@ -614,7 +614,7 @@ Rewrite H. Rewrite varlist_merge_ok. Repeat Rewrite (SR_distr_right T). Repeat Rewrite <- (SR_mult_assoc T). -Repeat Rewrite <- (SR_pus_assoc T). +Repeat Rewrite <- (SR_plus_assoc T). Reflexivity. Save. @@ -632,7 +632,7 @@ Rewrite H. Rewrite varlist_merge_ok. Repeat Rewrite (SR_distr_right T). Repeat Rewrite <- (SR_mult_assoc T). -Repeat Rewrite <- (SR_pus_assoc T). +Repeat Rewrite <- (SR_plus_assoc T). Rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)). Reflexivity. @@ -644,7 +644,7 @@ Rewrite H. Rewrite varlist_merge_ok. Repeat Rewrite (SR_distr_right T). Repeat Rewrite <- (SR_mult_assoc T). -Repeat Rewrite <- (SR_pus_assoc T). +Repeat Rewrite <- (SR_plus_assoc T). Rewrite (SR_mult_permute T c (interp_vl l) (interp_vl v)). Reflexivity. Save. |