diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-01 14:10:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-01 14:10:53 +0000 |
| commit | 7b03b26b4f652df0c2e55bd477a52b7e0547c438 (patch) | |
| tree | a1e6d5280a1f11175254ddfb2c98e95d4e801188 /contrib/ring/Ring_normalize.v | |
| parent | fc8427b6f806a240498f735eab8f32d6dc9552bd (diff) | |
De bizarres SR_pus_assoc au lieu de SR_plus_assoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1421 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring/Ring_normalize.v')
| -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 2590dd72b..536d2d303 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. |