ocaml 3.09 transition

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

diff --git a/helm/matita/library/nat/chinese_reminder.ma b/helm/matita/library/nat/chinese_reminder.ma
index f14f16d2792c3f2d291db23ee8d4586d9520df01..30cc7440f8a723d99fc1b6cd8371ce5bdbcf1931 100644 (file)
--- a/helm/matita/library/nat/chinese_reminder.ma
+++ b/helm/matita/library/nat/chinese_reminder.ma
@@ -53,7 +53,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* congruent to b *)
 cut (a2*m = a1*n - (S O)).
@@ -84,7 +84,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* and now the symmetric case; the price to pay for working
    in nat instead than Z *)
@@ -119,7 +119,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* congruent to a *)
 cut (a2*m = a1*n + (S O)).
@@ -149,7 +149,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* proof of the cut *)
 rewrite < H2.