X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Frings.ma;h=3ed2fab256bdb054ac4aa900842c2b6194c4ee81;hb=936f80cf031a7b034dd70fef49abb90e69f2e680;hp=ec460748baea730cf8cc347c572493f2e2ac8602;hpb=92682f04ee34e7fb98ee5311646aaa62838f1e17;p=helm.git

diff --git a/matita/dama/rings.ma b/matita/dama/rings.ma
index ec460748b..3ed2fab25 100644
--- a/matita/dama/rings.ma
+++ b/matita/dama/rings.ma
@@ -91,7 +91,8 @@ intros;
 generalize in match (zero_neutral R 0);
 intro;
 generalize in match (eq_f ? ? (λy.x*y) ? ? H); intro; clear H;
-rewrite > mult_plus_distr_left in H1;
+(*CSC: qua funzionava prima della patch all'unificazione!*)
+rewrite > (mult_plus_distr_left R) in H1;
 generalize in match (eq_f ? ? (λy. (-(x*0)) +y) ? ? H1);intro;
 clear H1;
 rewrite < plus_assoc in H;