ported to new syntactic requirement about terms being surrounded by parens

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

diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index 8c53a56c8adfb7872ffa6a846525edf58069cc60..70a4fd76ef5ab626a2d6a00d13fb075406c55f2a 100644 (file)
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -66,7 +66,7 @@ simplify.
 intros.elim x.
 simplify.reflexivity.
 simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
-apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z.
+apply eq_f.rewrite < assoc_plus. rewrite < (sym_plus ? z).
 rewrite > assoc_plus.reflexivity.
 qed.
 
@@ -79,7 +79,7 @@ elim x.simplify.apply refl_eq.
 simplify.rewrite < sym_times.
 rewrite > distr_times_plus.
 rewrite < sym_times.
-rewrite < sym_times (times n y) z.
+rewrite < (sym_times (times n y) z).
 rewrite < H.apply refl_eq.
 qed.