ocaml 3.09 transition

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

diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma
index ff425772cd276d31b239c15bb35d5f5e6345ef50..24c3920ed82571324c2977a7be798b492fbf43e7 100644 (file)
--- a/helm/matita/library/nat/totient.ma
+++ b/helm/matita/library/nat/totient.ma
@@ -68,35 +68,35 @@ rewrite < H4.
 rewrite > sym_gcd.
 rewrite > gcd_mod.
 apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite < H5.
 rewrite > sym_gcd.
 rewrite > gcd_mod.
 apply (gcd_times_SO_to_gcd_SO ? ? (S m)).
-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite > sym_times.
 assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 intro.
 apply eqb_elim.
 intro.apply eqb_elim.
 intro.apply False_ind.
 apply H6.
 apply eq_gcd_times_SO.
-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite < gcd_mod.
 rewrite > H4.
 rewrite > sym_gcd.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite < gcd_mod.
 rewrite > H5.
 rewrite > sym_gcd.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 intro.reflexivity.
 intro.reflexivity.
 qed.
\ No newline at end of file