ocaml 3.09 transition

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

diff --git a/helm/matita/library/nat/congruence.ma b/helm/matita/library/nat/congruence.ma
index 6bc2b6f689bc5d6266651ebc41e6c09bffeb0250..af744cf3475087290d2100638f3a6af3b729c732 100644 (file)
--- a/helm/matita/library/nat/congruence.ma
+++ b/helm/matita/library/nat/congruence.ma
@@ -54,8 +54,8 @@ qed.
 
 theorem mod_times_mod : \forall n,m,p:nat. O<p \to O<m \to n \mod p = (n \mod (m*p)) \mod p.
 intros.
-apply div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
-(n/(m*p)*m + (n \mod (m*p)/p)).
+apply (div_mod_spec_to_eq2 n p (n/p) (n \mod p) 
+(n/(m*p)*m + (n \mod (m*p)/p))).
 apply div_mod_spec_div_mod.assumption.
 constructor 1.
 apply lt_mod_m_m.assumption.
@@ -65,7 +65,7 @@ rewrite < div_mod.
 rewrite > assoc_times.
 rewrite < div_mod.
 reflexivity.
-rewrite > times_n_O O.
+rewrite > (times_n_O O).
 apply lt_times.
 assumption.assumption.assumption.
 qed.