Parentheses must now be put in patterns like in tactic arguments.

[helm.git] / helm / matita / library / Z / times.ma

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 19158e300bec21656616171ff60a1052c4007ec7..27266bf393c41e5457f5cd6723bb8276035df5c6 100644 (file)
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -148,8 +148,8 @@ lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q). 
 intros.
 simplify. 
-change in match p + n * (S p) with (pred ((S n) * (S p))).
-change in match q + n * (S q) with (pred ((S n) * (S q))).
+change in match (p + n * (S p)) with (pred ((S n) * (S p))).
+change in match (q + n * (S q)) with (pred ((S n) * (S q))).
 rewrite < nat_compare_pred_pred.
 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.