From 7b03b26b4f652df0c2e55bd477a52b7e0547c438 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 1 Mar 2001 14:10:53 +0000
Subject: 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
---
 contrib/ring/Ring_normalize.v | 8 ++++----
 1 file 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.
-- 
cgit v1.2.3