ocaml 3.09 transition

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

diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma
index 331df8fb3c4fa426b369d770604dff0ec90f1eb7..4f5f6cba008299370b94fb0e95f7b0b6248407a6 100644 (file)
--- a/helm/matita/library/nat/sigma_and_pi.ma
+++ b/helm/matita/library/nat/sigma_and_pi.ma
@@ -36,8 +36,8 @@ intros 3.elim n.
 simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n.
 simplify.
 apply eq_f2.apply H1.
-change with m \le (S n1)+m.apply le_plus_n.
-rewrite > sym_plus m.apply le_n.
+change with (m \le (S n1)+m).apply le_plus_n.
+rewrite > (sym_plus m).apply le_n.
 apply H.intros.apply H1.assumption.
 rewrite < plus_n_Sm.
 apply le_S.assumption.
@@ -51,8 +51,8 @@ intros 3.elim n.
 simplify.apply H.apply le_n.rewrite < plus_n_O.apply le_n.
 simplify.
 apply eq_f2.apply H1.
-change with m \le (S n1)+m.apply le_plus_n.
-rewrite > sym_plus m.apply le_n.
+change with (m \le (S n1)+m).apply le_plus_n.
+rewrite > (sym_plus m).apply le_n.
 apply H.intros.apply H1.assumption.
 rewrite < plus_n_Sm.
 apply le_S.assumption.
@@ -61,7 +61,7 @@ qed.
 theorem eq_fact_pi: \forall n. (S n)! = pi n (\lambda m.m) (S O).
 intro.elim n.
 simplify.reflexivity.
-change with (S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O)).
+change with ((S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O))).
 rewrite < plus_n_Sm.rewrite < plus_n_O.
 apply eq_f.assumption.
 qed.