Adapt to coq/coq#18590

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]

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;

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)^+;

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}.