X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2FQ%2Fq.ma;h=07a992926f1a434d5f01fc20f1873f27a3da3963;hb=f764844fa35ab0bb9c10707151340b924060f069;hp=af0161c2ac1f885a9c22edb80d672018cc09d875;hpb=49f8a041ca862b3fb93c277737c2e7aa02bc4b4e;p=helm.git

diff --git a/matita/library/Q/q.ma b/matita/library/Q/q.ma
index af0161c2a..07a992926 100644
--- a/matita/library/Q/q.ma
+++ b/matita/library/Q/q.ma
@@ -262,6 +262,7 @@ unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes
   intros.change with (frac (cons (x1 + neg m) f) = frac (cons (neg m + x1) f)).
    rewrite < sym_Zplus.reflexivity.
   intros.
+   (*CSC: simplify does something nasty here because of a redex in Zplus *)
    change with 
    (match ftimes f g with
    [ one \Rightarrow Z_to_ratio (x1 + y1)
@@ -278,6 +279,7 @@ intro.elim f.
    rewrite > Zplus_Zopp.reflexivity.
   change with (Z_to_ratio (neg n + - (neg n)) = one).
    rewrite > Zplus_Zopp.reflexivity.
+   (*CSC: simplify does something nasty here because of a redex in Zplus *)
 (* again: we would need something to help finding the right change *)
   change with 
   (match ftimes f1 (finv f1) with