From c2cb8fda59ca04f9cd2d26a3997d5a16edb59d4c Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre@roux01.fr>
Date: Wed, 31 Jan 2024 21:00:19 +0100
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18590

---
 theories/kat.v     |  6 +++---
 theories/lattice.v |  2 +-
 theories/monoid.v  |  6 +++---
 theories/relalg.v  | 24 ++++++++++++------------
 4 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/theories/kat.v b/theories/kat.v
index d22f76f..2bd43c2 100644
--- a/theories/kat.v
+++ b/theories/kat.v
@@ -41,7 +41,7 @@ Notation " [ p ] " := (inj p): ra_terms.
    injection should be a morphism of idempotent semirings, i.e, map 
    [(leq,weq,cap,cup,top,bot)] into [(leq,weq,dot,pls,one,zer)] *)
 
-(* TOTHINK: voir si on laisse les deux instances :>, 
+(* TOTHINK: voir si on laisse les deux instances ::, 
    qui ne sont utiles que dans l'abstrait si les structures 
    concrètes sont déclarées incrémentalement 
    voir aussi s'il ne vaut pas mieux poser ces deux instances en
@@ -50,8 +50,8 @@ Notation " [ p ] " := (inj p): ra_terms.
    TODO: relacher les contraintes sur les niveaux
 *)
 Class laws (X: ops) := {
-  kar_BKA:> monoid.laws BKA kar;
-  tst_BL:> forall n, lattice.laws BL (tst n);
+  kar_BKA:: monoid.laws BKA kar;
+  tst_BL:: forall n, lattice.laws BL (tst n);
   mor_inj: forall n, morphism BSL (@inj X n);
   inj_top: forall n, [top] ≡ one n;
   inj_cap: forall n (p q: tst n), [p ⊓ q] ≡ [p] ⋅ [q]
diff --git a/theories/lattice.v b/theories/lattice.v
index 206f322..328d320 100644
--- a/theories/lattice.v
+++ b/theories/lattice.v
@@ -94,7 +94,7 @@ Notation "! x" := (neg x) (right associativity, at level 20, format "! x"): ra_t
    typeclass resolution. *)
 
 Class laws (l: level) (X: ops) := {
-  leq_PreOrder:> PreOrder leq;
+  leq_PreOrder:: PreOrder leq;
   weq_spec            : forall x y , x ≡ y <-> x ≦ y /\ y ≦ x;
   cup_spec {Hl:CUP ≪ l}: forall x y z, x ⊔ y ≦ z <-> x ≦ z /\ y ≦ z;
   cap_spec {Hl:CAP ≪ l}: forall x y z, z ≦ x ⊓ y <-> z ≦ x /\ z ≦ y;
diff --git a/theories/monoid.v b/theories/monoid.v
index e57a2ab..f15e399 100644
--- a/theories/monoid.v
+++ b/theories/monoid.v
@@ -96,7 +96,7 @@ Unset Strict Implicit.
    typeclass resolution. *)
 
 Class laws (l: level) (X: ops) := {
-  lattice_laws:>       forall n m, lattice.laws l (X n m);
+  lattice_laws::       forall n m, lattice.laws l (X n m);
   (** po-monoid laws *)
   dotA:                forall n m p q (x: X n m) y (z: X p q), x⋅(y⋅z) ≡ (x⋅y)⋅z;
   dot1x:               forall n m (x: X n m), 1⋅x ≡ x;
@@ -110,7 +110,7 @@ Class laws (l: level) (X: ops) := {
   (** converse laws *)
   cnvdot_   `{CNV ≪ l}: forall n m p (x: X n m) (y: X m p), (x⋅y)° ≦ y°⋅x°;
   cnv_invol `{CNV ≪ l}: forall n m (x: X n m), x°° ≡ x;
-  cnv_leq   `{CNV ≪ l}:>forall n m, Proper (leq ==> leq) (cnv n m);
+  cnv_leq   `{CNV ≪ l}::forall n m, Proper (leq ==> leq) (cnv n m);
   cnv_ext_  `{CNV ≪ l}: CAP ≪ l \/ forall n m (x: X n m), x ≦ x⋅x°⋅x;
   (** star laws *)
   str_refl  `{STR ≪ l}: forall n (x: X n n), 1 ≦ x^*;
@@ -456,7 +456,7 @@ Proof. dual @Schroeder_l. Qed.
 (** * Functors (i.e., monoid morphisms) *)
 
 Class functor l {X Y: ops} (f': ob X -> ob Y) (f: forall {n m}, X n m -> Y (f' n) (f' m)) := {
-  fn_morphism:>     forall n m, morphism l (@f n m);
+  fn_morphism::     forall n m, morphism l (@f n m);
   fn_dot:           forall n m p (x: X n m) (y: X m p), f (x⋅y) ≡ f x ⋅ f y;
   fn_one:           forall n, f (one n) ≡ 1;
   fn_itr `{STR ≪ l}: forall n (x: X n n), f (x^+) ≡ (f x)^+;
diff --git a/theories/relalg.v b/theories/relalg.v
index f3295e8..3ea8180 100644
--- a/theories/relalg.v
+++ b/theories/relalg.v
@@ -66,30 +66,30 @@ Class is_total n m (x: X n m) := total: 1 ≦ x ⋅ x°.
 Class is_vector n m (v: X n m) := vector: v⋅top ≡ v.
 
 Class is_point n m (p: X n m) := {
-  point_vector:> is_vector p;
-  point_injective:> is_injective p;
-  point_nonempty:> is_nonempty p}.
+  point_vector:: is_vector p;
+  point_injective:: is_injective p;
+  point_nonempty:: is_nonempty p}.
 
 Class is_atom n m (a: X n m) := {
   a_top_a': a⋅top⋅a° ≦ 1;
   a'_top_a: a°⋅top⋅a ≦ 1;
-  atom_nonempty:> is_nonempty a}.
+  atom_nonempty:: is_nonempty a}.
 
 Class is_mapping n m (f: X n m) := {
-  mapping_univalent:> is_univalent f;
-  mapping_total:> is_total f}.
+  mapping_univalent:: is_univalent f;
+  mapping_total:: is_total f}.
 
 Class is_per n (e: X n n) := {
-  per_symmetric:> is_symmetric e;
-  per_transitive:> is_transitive e}.
+  per_symmetric:: is_symmetric e;
+  per_transitive:: is_transitive e}.
 
 Class is_preorder n (p: X n n) := {
-  pre_reflexive:> is_reflexive p;
-  pre_transitive:> is_transitive p}.
+  pre_reflexive:: is_reflexive p;
+  pre_transitive:: is_transitive p}.
 
 Class is_order n (p: X n n) := {
-  ord_preorder:> is_preorder p;
-  ord_antisymmetric:> is_antisymmetric p}.
+  ord_preorder:: is_preorder p;
+  ord_antisymmetric:: is_antisymmetric p}.
 
 Context {L: laws l X}.