From a02199df46bad0cfdca3df01d97be61095c7686d Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Mon, 25 Nov 2024 15:38:18 +0100
Subject: [PATCH] adapt to mc#1256

---
 theories/normedtype.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/normedtype.v b/theories/normedtype.v
index bf18d7bcd..ad227e6e1 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -244,11 +244,11 @@ Proof.
 apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]].
   exists (-%R @` A).
     exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//.
-    by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC.
+    by apply: reA; rewrite ?(@eqr_opp R)//= opprK addrC distrC.
   rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=.
   by rewrite opprK.
 exists e => //= x/=; rewrite -opprD normrN => axe xa.
-exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=.
+exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?(@eqr_oppLR R)//=.
 by rewrite opprK.
 Qed.