From 05883b9a7805c13b3fc7b10bf85b6c90d123c998 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 31 Jan 2024 12:18:40 +0100
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18590

---
 theories/Programming/Eqv.v   | 6 ++++--
 theories/Programming/Le.v    | 6 ++++--
 theories/Structures/Monoid.v | 9 ++++++---
 3 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/theories/Programming/Eqv.v b/theories/Programming/Eqv.v
index 8bcd804a..72d710d9 100644
--- a/theories/Programming/Eqv.v
+++ b/theories/Programming/Eqv.v
@@ -6,9 +6,11 @@ Class Eqv T := eqv : T -> T -> Prop.
 Definition neg_eqv {T} {E:Eqv T} (x:T) (y:T) : Prop := not (eqv x y).
 
 Class EqvWF T :=
-{ eqvWFEqv :> Eqv T
-; eqvWFEquivalence :> Equivalence eqv
+{ eqvWFEqv : Eqv T
+; eqvWFEquivalence : Equivalence eqv
 }.
+#[global] Existing Instance eqvWFEqv.
+#[global] Existing Instance eqvWFEquivalence.
 #[global]
 Instance EqvWF_Build {T} {E:Eqv T} {EV:Equivalence eqv} : EqvWF T :=
   { eqvWFEqv := E ; eqvWFEquivalence := EV }.
diff --git a/theories/Programming/Le.v b/theories/Programming/Le.v
index 017fe04d..2b4d019f 100644
--- a/theories/Programming/Le.v
+++ b/theories/Programming/Le.v
@@ -27,9 +27,11 @@ Proof. constructor.
 Qed.
 
 Class LteWF T :=
-{ lteWFLte :> Lte T
-; lteWFPreOrder :> PreOrder lte
+{ lteWFLte : Lte T
+; lteWFPreOrder : PreOrder lte
 }.
+#[global] Existing Instance lteWFLte.
+#[global] Existing Instance lteWFPreOrder.
 
 #[global]
 Instance LteWF_Build {T} {L:Lte T} {PO:PreOrder lte} : LteWF T :=
diff --git a/theories/Structures/Monoid.v b/theories/Structures/Monoid.v
index ad73f08b..b9d574b5 100644
--- a/theories/Structures/Monoid.v
+++ b/theories/Structures/Monoid.v
@@ -14,9 +14,12 @@ Section Monoid.
   }.
 
   Class MonoidLaws@{} (M : Monoid) : Type :=
-  { monoid_assoc :> Associative M.(monoid_plus) eq
-  ; monoid_lunit :> LeftUnit M.(monoid_plus) M.(monoid_unit) eq
-  ; monoid_runit :> RightUnit M.(monoid_plus) M.(monoid_unit) eq
+  { monoid_assoc : Associative M.(monoid_plus) eq
+  ; monoid_lunit : LeftUnit M.(monoid_plus) M.(monoid_unit) eq
+  ; monoid_runit : RightUnit M.(monoid_plus) M.(monoid_unit) eq
   }.
+  #[global] Existing Instance monoid_assoc.
+  #[global] Existing Instance monoid_lunit.
+  #[global] Existing Instance monoid_runit.
 
 End Monoid.