X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Frings.ma;h=3ed2fab256bdb054ac4aa900842c2b6194c4ee81;hb=66faca1dc849662e27d760b950294ef66a5741b3;hp=a562a48192613192265518445b7d313553c5e29f;hpb=85fce74d6a0cd8e83e59895e81f1bc09d21ef4c2;p=helm.git

diff --git a/helm/software/matita/dama/rings.ma b/helm/software/matita/dama/rings.ma
index a562a4819..3ed2fab25 100644
--- a/helm/software/matita/dama/rings.ma
+++ b/helm/software/matita/dama/rings.ma
@@ -90,9 +90,10 @@ lemma eq_mult_x_zero_zero: ∀R:ring.∀x:R.x*0=0.
 intros;
 generalize in match (zero_neutral R 0);
 intro;
-generalize in match (eq_f ? ? (\lambda y.x*y) ? ? H); intro; clear H;
-rewrite > mult_plus_distr_left in H1;
-generalize in match (eq_f ? ? (\lambda y. (-(x*0)) +y) ? ? H1);intro;
+generalize in match (eq_f ? ? (λy.x*y) ? ? H); intro; clear H;
+(*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;
 rewrite > opp_inverse in H;