diff --git a/accuracy_proofs/gemv_acc.v b/accuracy_proofs/gemv_acc.v
index 7ccdf00..9d60e36 100644
--- a/accuracy_proofs/gemv_acc.v
+++ b/accuracy_proofs/gemv_acc.v
@@ -333,7 +333,7 @@ apply ler_pmul => //.
 apply normM_pos.
 apply normv_pos.
 rewrite /normM mulrC big_max_mul.
-apply le_bigmax2 => i0 _. 
+apply: le_bigmax2 => i0 _.
 rewrite /sum_abs.
 rewrite big_mul =>  [ | i b | ]; try ring.
 apply ler_sum => i _.
@@ -349,4 +349,4 @@ rewrite Hlenv1 in H2.
 apply H2.
 Qed.
 
-End ForwardError. 
\ No newline at end of file
+End ForwardError.
diff --git a/accuracy_proofs/mv_mathcomp.v b/accuracy_proofs/mv_mathcomp.v
index 0922b64..cdef879 100644
--- a/accuracy_proofs/mv_mathcomp.v
+++ b/accuracy_proofs/mv_mathcomp.v
@@ -614,7 +614,7 @@ Lemma subMultNorm m (A: 'M[R]_m.+1)  (u : 'cV_m.+1) :
 Proof.
 remember (normv u) as umax.
 rewrite /normr /normM /normv /sum_abs /= big_max_mul.
-apply le_bigmax2 => i0 _. 
+apply: le_bigmax2 => i0 _.
 rewrite mxE => /=.
 eapply le_trans.
 apply Rabs_sum .