From 7e5c81dcfafde501e87a2c2db4021f5190dff960 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 22 Aug 2023 21:56:25 -0700
Subject: [PATCH] Fix unification errors

I need these changes for LAProof to build on my configuration.  Not sure
which particular version needs this (Coq 8.18?)
---
 accuracy_proofs/gemv_acc.v    | 4 ++--
 accuracy_proofs/mv_mathcomp.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

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 .