diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 65851c1..2246da3 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -18,14 +18,8 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.19'
           - 'coqorg/coq:8.18'
-          - 'coqorg/coq:8.17'
-          - 'coqorg/coq:8.16'
-          - 'coqorg/coq:8.15'
-          - 'coqorg/coq:8.14'
-          - 'coqorg/coq:8.13'
-          - 'coqorg/coq:8.12'
-          - 'coqorg/coq:8.11'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
diff --git a/README.md b/README.md
index 9e59e83..fa7bd90 100644
--- a/README.md
+++ b/README.md
@@ -10,8 +10,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Zulip][zulip-shield]][zulip-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/math-classes/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/math-classes/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/math-classes/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/math-classes/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -50,7 +50,7 @@ notations.
 - Coq-community maintainer(s):
   - Bas Spitters ([**@spitters**](https://github.com/spitters))
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: Coq 8.11 or later (use releases for other Coq versions)
+- Compatible Coq versions: Coq 8.18 or later (use releases for other Coq versions)
 - Additional dependencies:
   - [BigNums](https://github.com/coq/bignums)
 - Coq namespace: `MathClasses`
diff --git a/coq-math-classes.opam b/coq-math-classes.opam
index 39c527c..9c5c029 100644
--- a/coq-math-classes.opam
+++ b/coq-math-classes.opam
@@ -30,7 +30,7 @@ build: [
 ]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.11" & < "8.19~") | (= "dev")}
+  "coq" {(>= "8.18" & < "8.20~") | (= "dev")}
   "coq-bignums" 
 ]
 
diff --git a/implementations/fast_rationals.v b/implementations/fast_rationals.v
index fa07d45..7adb506 100644
--- a/implementations/fast_rationals.v
+++ b/implementations/fast_rationals.v
@@ -1,8 +1,9 @@
 Require
+  MathClasses.theory.rings
   MathClasses.theory.shiftl MathClasses.theory.int_pow.
 Require Import
   Coq.QArith.QArith Bignums.BigQ.BigQ
-  MathClasses.interfaces.abstract_algebra
+  MathClasses.interfaces.orders MathClasses.interfaces.abstract_algebra MathClasses.interfaces.naturals
   MathClasses.interfaces.integers MathClasses.interfaces.rationals MathClasses.interfaces.additional_operations
   MathClasses.implementations.fast_naturals MathClasses.implementations.fast_integers MathClasses.implementations.field_of_fractions MathClasses.implementations.stdlib_rationals.
 Require Export
diff --git a/interfaces/abstract_algebra.v b/interfaces/abstract_algebra.v
index b63b504..4c2f61f 100644
--- a/interfaces/abstract_algebra.v
+++ b/interfaces/abstract_algebra.v
@@ -6,9 +6,9 @@ For various structures we omit declaration of substructures. For example, if we
 say:
 
 Class Setoid_Morphism :=
-  { setoidmor_a :> Setoid A
-  ; setoidmor_b :> Setoid B
-  ; sm_proper :> Proper ((=) ==> (=)) f }.
+  { setoidmor_a :: Setoid A
+  ; setoidmor_b :: Setoid B
+  ; sm_proper :: Proper ((=) ==> (=)) f }.
 
 then each time a Setoid instance is required, Coq will try to prove that a
 Setoid_Morphism exists. This obviously results in an enormous blow-up of the
@@ -20,14 +20,14 @@ Setoid_Morphism as a substructure, setoid rewriting will become horribly slow.
 *)
 
 (* An unbundled variant of the former CoRN RSetoid *)
-Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :> Equivalence (@equiv A Ae).
+Class Setoid A {Ae : Equiv A} : Prop := setoid_eq :: Equivalence (@equiv A Ae).
 
 (* An unbundled variant of the former CoRN CSetoid. We do not 
   include a proof that A is a Setoid because it can be derived. *)
 Class StrongSetoid A {Ae : Equiv A} `{Aap : Apart A} : Prop :=
-  { strong_setoid_irreflexive :> Irreflexive (≶) 
-  ; strong_setoid_symmetric :> Symmetric (≶) 
-  ; strong_setoid_cotrans :> CoTransitive (≶) 
+  { strong_setoid_irreflexive :: Irreflexive (≶)
+  ; strong_setoid_symmetric :: Symmetric (≶)
+  ; strong_setoid_cotrans :: CoTransitive (≶)
   ; tight_apart : ∀ x y, ¬x ≶ y ↔ x = y }.
 
 Arguments tight_apart {A Ae Aap StrongSetoid} _ _.
@@ -38,7 +38,7 @@ Section setoid_morphisms.
   Class Setoid_Morphism :=
     { setoidmor_a : Setoid A
     ; setoidmor_b : Setoid B
-    ; sm_proper :> Proper ((=) ==> (=)) f }. 
+    ; sm_proper :: Proper ((=) ==> (=)) f }.
 
   Class StrongSetoid_Morphism :=
     { strong_setoidmor_a : StrongSetoid A
@@ -70,55 +70,55 @@ Section upper_classes.
   Context A {Ae : Equiv A}.
 
   Class SemiGroup {Aop: SgOp A} : Prop :=
-    { sg_setoid :> Setoid A
-    ; sg_ass :> Associative (&)
-    ; sg_op_proper :> Proper ((=) ==> (=) ==> (=)) (&) }.
+    { sg_setoid :: Setoid A
+    ; sg_ass :: Associative (&)
+    ; sg_op_proper :: Proper ((=) ==> (=) ==> (=)) (&) }.
 
   Class CommutativeSemiGroup {Aop : SgOp A} : Prop :=
-    { comsg_setoid :> @SemiGroup Aop
-    ; comsg_ass :> Commutative (&) }.
+    { comsg_setoid :: @SemiGroup Aop
+    ; comsg_ass :: Commutative (&) }.
 
   Class SemiLattice {Aop : SgOp A} : Prop :=
-    { semilattice_sg :> @CommutativeSemiGroup Aop
-    ; semilattice_idempotent :> BinaryIdempotent (&)}.
+    { semilattice_sg :: @CommutativeSemiGroup Aop
+    ; semilattice_idempotent :: BinaryIdempotent (&)}.
 
   Class Monoid {Aop : SgOp A} {Aunit : MonUnit A} : Prop :=
-    { monoid_semigroup :> SemiGroup
-    ; monoid_left_id :> LeftIdentity (&) mon_unit
-    ; monoid_right_id :> RightIdentity (&) mon_unit }.
+    { monoid_semigroup :: SemiGroup
+    ; monoid_left_id :: LeftIdentity (&) mon_unit
+    ; monoid_right_id :: RightIdentity (&) mon_unit }.
 
   Class CommutativeMonoid {Aop Aunit} : Prop :=
-    { commonoid_mon :> @Monoid Aop Aunit
-    ; commonoid_commutative :> Commutative (&) }.
+    { commonoid_mon :: @Monoid Aop Aunit
+    ; commonoid_commutative :: Commutative (&) }.
 
   Class Group {Aop Aunit} {Anegate : Negate A} : Prop :=
-    { group_monoid :> @Monoid Aop Aunit
-    ; negate_proper :> Setoid_Morphism (-)
-    ; negate_l :> LeftInverse (&) (-) mon_unit
-    ; negate_r :> RightInverse (&) (-) mon_unit }.
+    { group_monoid :: @Monoid Aop Aunit
+    ; negate_proper :: Setoid_Morphism (-)
+    ; negate_l :: LeftInverse (&) (-) mon_unit
+    ; negate_r :: RightInverse (&) (-) mon_unit }.
 
   Class BoundedSemiLattice {Aop Aunit} : Prop :=
-    { bounded_semilattice_mon :> @CommutativeMonoid Aop Aunit
-    ; bounded_semilattice_idempotent :> BinaryIdempotent (&)}.
+    { bounded_semilattice_mon :: @CommutativeMonoid Aop Aunit
+    ; bounded_semilattice_idempotent :: BinaryIdempotent (&)}.
 
   Class AbGroup {Aop Aunit Anegate} : Prop :=
-    { abgroup_group :> @Group Aop Aunit Anegate
-    ; abgroup_commutative :> Commutative (&) }.
+    { abgroup_group :: @Group Aop Aunit Anegate
+    ; abgroup_commutative :: Commutative (&) }.
 
   Context {Aplus : Plus A} {Amult : Mult A} {Azero : Zero A} {Aone : One A}.
 
   Class SemiRing : Prop :=
-    { semiplus_monoid :> @CommutativeMonoid plus_is_sg_op zero_is_mon_unit
-    ; semimult_monoid :> @CommutativeMonoid mult_is_sg_op one_is_mon_unit
-    ; semiring_distr :> LeftDistribute (.*.) (+)
-    ; semiring_left_absorb :> LeftAbsorb (.*.) 0 }.
+    { semiplus_monoid :: @CommutativeMonoid plus_is_sg_op zero_is_mon_unit
+    ; semimult_monoid :: @CommutativeMonoid mult_is_sg_op one_is_mon_unit
+    ; semiring_distr :: LeftDistribute (.*.) (+)
+    ; semiring_left_absorb :: LeftAbsorb (.*.) 0 }.
 
   Context {Anegate : Negate A}.
 
   Class Ring : Prop :=
-    { ring_group :> @AbGroup plus_is_sg_op zero_is_mon_unit _
-    ; ring_monoid :> @CommutativeMonoid mult_is_sg_op one_is_mon_unit
-    ; ring_dist :> LeftDistribute (.*.) (+) }.
+    { ring_group :: @AbGroup plus_is_sg_op zero_is_mon_unit _
+    ; ring_monoid :: @CommutativeMonoid mult_is_sg_op one_is_mon_unit
+    ; ring_dist :: LeftDistribute (.*.) (+) }.
 
   (* For now, we follow CoRN/ring_theory's example in having Ring and SemiRing
     require commutative multiplication. *)
@@ -126,24 +126,24 @@ Section upper_classes.
   Class IntegralDomain : Prop :=
     { intdom_ring : Ring 
     ; intdom_nontrivial : PropHolds (1 ≠ 0)
-    ; intdom_nozeroes :> NoZeroDivisors A }.
+    ; intdom_nozeroes :: NoZeroDivisors A }.
 
   (* We do not include strong extensionality for (-) and (/) because it can de derived *)
   Class Field {Aap: Apart A} {Arecip: Recip A} : Prop :=
-    { field_ring :> Ring
-    ; field_strongsetoid :> StrongSetoid A
-    ; field_plus_ext :> StrongSetoid_BinaryMorphism (+)
-    ; field_mult_ext :> StrongSetoid_BinaryMorphism (.*.)
+    { field_ring :: Ring
+    ; field_strongsetoid :: StrongSetoid A
+    ; field_plus_ext :: StrongSetoid_BinaryMorphism (+)
+    ; field_mult_ext :: StrongSetoid_BinaryMorphism (.*.)
     ; field_nontrivial : PropHolds (1 ≶ 0)
-    ; recip_proper :> Setoid_Morphism (//)
+    ; recip_proper :: Setoid_Morphism (//)
     ; recip_inverse : ∀ x, `x // x = 1 }.
 
   (* We let /0 = 0 so properties as Injective (/), f (/x) = / (f x), / /x = x, /x * /y = /(x * y) 
     hold without any additional assumptions *)
   Class DecField {Adec_recip : DecRecip A} : Prop :=
-    { decfield_ring :> Ring
+    { decfield_ring :: Ring
     ; decfield_nontrivial : PropHolds (1 ≠ 0)
-    ; dec_recip_proper :> Setoid_Morphism (/)
+    ; dec_recip_proper :: Setoid_Morphism (/)
     ; dec_recip_0 : /0 = 0
     ; dec_recip_inverse : ∀ x, x ≠ 0 → x / x = 1 }.
 End upper_classes.
@@ -159,7 +159,7 @@ Hint Extern 5 (PropHolds (1 ≠ 0)) => eapply @decfield_nontrivial : typeclass_i
 (* 
 For a strange reason Ring instances of Integers are sometimes obtained by
 Integers -> IntegralDomain -> Ring and sometimes directly. Making this an
-instance with a low priority instead of using intdom_ring:> Ring forces Coq to
+instance with a low priority instead of using intdom_ring:: Ring forces Coq to
 take the right way 
 *)
 #[global]
@@ -174,29 +174,29 @@ Section lattice.
   Context A `{Ae: Equiv A} {Ajoin: Join A} {Ameet: Meet A} `{Abottom : Bottom A}.
 
   Class JoinSemiLattice : Prop := 
-    join_semilattice :> @SemiLattice A Ae join_is_sg_op.
+    join_semilattice :: @SemiLattice A Ae join_is_sg_op.
   Class BoundedJoinSemiLattice : Prop := 
-    bounded_join_semilattice :> @BoundedSemiLattice A Ae join_is_sg_op bottom_is_mon_unit.
+    bounded_join_semilattice :: @BoundedSemiLattice A Ae join_is_sg_op bottom_is_mon_unit.
   Class MeetSemiLattice : Prop := 
-    meet_semilattice :> @SemiLattice A Ae meet_is_sg_op.
+    meet_semilattice :: @SemiLattice A Ae meet_is_sg_op.
 
   Class Lattice : Prop := 
-    { lattice_join :> JoinSemiLattice
-    ; lattice_meet :> MeetSemiLattice
-    ; join_meet_absorption :> Absorption (⊔) (⊓) 
-    ; meet_join_absorption :> Absorption (⊓) (⊔)}.
+    { lattice_join :: JoinSemiLattice
+    ; lattice_meet :: MeetSemiLattice
+    ; join_meet_absorption :: Absorption (⊔) (⊓) 
+    ; meet_join_absorption :: Absorption (⊓) (⊔)}.
 
   Class DistributiveLattice : Prop := 
-    { distr_lattice_lattice :> Lattice
-    ; join_meet_distr_l :> LeftDistribute (⊔) (⊓) }.
+    { distr_lattice_lattice :: Lattice
+    ; join_meet_distr_l :: LeftDistribute (⊔) (⊓) }.
 End lattice.
 
 Class Category O `{!Arrows O} `{∀ x y: O, Equiv (x ⟶ y)} `{!CatId O} `{!CatComp O}: Prop :=
-  { arrow_equiv :> ∀ x y, Setoid (x ⟶ y)
-  ; comp_proper :> ∀ x y z, Proper ((=) ==> (=) ==> (=)) (comp x y z)
-  ; comp_assoc :> ArrowsAssociative O
-  ; id_l :> ∀ x y, LeftIdentity (comp x y y) cat_id
-  ; id_r :> ∀ x y, RightIdentity (comp x x y) cat_id }.
+  { arrow_equiv :: ∀ x y, Setoid (x ⟶ y)
+  ; comp_proper :: ∀ x y z, Proper ((=) ==> (=) ==> (=)) (comp x y z)
+  ; comp_assoc :: ArrowsAssociative O
+  ; id_l :: ∀ x y, LeftIdentity (comp x y y) cat_id
+  ; id_r :: ∀ x y, RightIdentity (comp x x y) cat_id }.
       (* note: no equality on objects. *)
 
 (* todo: use my comp everywhere *)
@@ -208,46 +208,46 @@ Section morphism_classes.
   Class SemiGroup_Morphism {Aop Bop} (f : A → B) :=
     { sgmor_a : @SemiGroup A Ae Aop
     ; sgmor_b : @SemiGroup B Be Bop
-    ; sgmor_setmor :> Setoid_Morphism f
+    ; sgmor_setmor :: Setoid_Morphism f
     ; preserves_sg_op : ∀ x y, f (x & y) = f x & f y }.
 
   Class JoinSemiLattice_Morphism {Ajoin Bjoin} (f : A → B) :=
     { join_slmor_a : @JoinSemiLattice A Ae Ajoin
     ; join_slmor_b : @JoinSemiLattice B Be Bjoin
-    ; join_slmor_sgmor :> @SemiGroup_Morphism join_is_sg_op join_is_sg_op f }.
+    ; join_slmor_sgmor :: @SemiGroup_Morphism join_is_sg_op join_is_sg_op f }.
 
   Class MeetSemiLattice_Morphism {Ameet Bmeet} (f : A → B) :=
     { meet_slmor_a : @MeetSemiLattice A Ae Ameet
     ; meet_slmor_b : @MeetSemiLattice B Be Bmeet
-    ; meet_slmor_sgmor :> @SemiGroup_Morphism meet_is_sg_op meet_is_sg_op f }.
+    ; meet_slmor_sgmor :: @SemiGroup_Morphism meet_is_sg_op meet_is_sg_op f }.
 
   Class Monoid_Morphism {Aunit Bunit Aop Bop} (f : A → B) :=
     { monmor_a : @Monoid A Ae Aop Aunit
     ; monmor_b : @Monoid B Be Bop Bunit
-    ; monmor_sgmor :> SemiGroup_Morphism f
+    ; monmor_sgmor :: SemiGroup_Morphism f
     ; preserves_mon_unit : f mon_unit = mon_unit }.
 
   Class BoundedJoinSemiLattice_Morphism {Abottom Bbottom Ajoin Bjoin} (f : A → B) :=
     { bounded_join_slmor_a : @BoundedJoinSemiLattice A Ae Ajoin Abottom
     ; bounded_join_slmor_b : @BoundedJoinSemiLattice B Be Bjoin Bbottom
-    ; bounded_join_slmor_monmor :> @Monoid_Morphism bottom_is_mon_unit bottom_is_mon_unit join_is_sg_op join_is_sg_op f }.
+    ; bounded_join_slmor_monmor :: @Monoid_Morphism bottom_is_mon_unit bottom_is_mon_unit join_is_sg_op join_is_sg_op f }.
 
   Class SemiRing_Morphism {Aplus Amult Azero Aone Bplus Bmult Bzero Bone} (f : A → B) :=
     { semiringmor_a : @SemiRing A Ae Aplus Amult Azero Aone
     ; semiringmor_b : @SemiRing B Be Bplus Bmult Bzero Bone
-    ; semiringmor_plus_mor :> @Monoid_Morphism zero_is_mon_unit zero_is_mon_unit plus_is_sg_op plus_is_sg_op f
-    ; semiringmor_mult_mor :> @Monoid_Morphism one_is_mon_unit one_is_mon_unit mult_is_sg_op mult_is_sg_op f }.
+    ; semiringmor_plus_mor :: @Monoid_Morphism zero_is_mon_unit zero_is_mon_unit plus_is_sg_op plus_is_sg_op f
+    ; semiringmor_mult_mor :: @Monoid_Morphism one_is_mon_unit one_is_mon_unit mult_is_sg_op mult_is_sg_op f }.
 
   Class Lattice_Morphism {Ajoin Ameet Bjoin Bmeet} (f : A → B) :=
     { latticemor_a : @Lattice A Ae Ajoin Ameet
     ; latticemor_b : @Lattice B Be Bjoin Bmeet
-    ; latticemor_join_mor :> JoinSemiLattice_Morphism f
-    ; latticemor_meet_mor :> MeetSemiLattice_Morphism f }.
+    ; latticemor_join_mor :: JoinSemiLattice_Morphism f
+    ; latticemor_meet_mor :: MeetSemiLattice_Morphism f }.
 
   Context {Aap : Apart A} {Bap : Apart B}.
   Class StrongSemiRing_Morphism {Aplus Amult Azero Aone Bplus Bmult Bzero Bone} (f : A → B) :=
-    { strong_semiringmor_sr_mor :> @SemiRing_Morphism Aplus Amult Azero Aone Bplus Bmult Bzero Bone f
-    ; strong_semiringmor_strong_mor :> StrongSetoid_Morphism f }.
+    { strong_semiringmor_sr_mor :: @SemiRing_Morphism Aplus Amult Azero Aone Bplus Bmult Bzero Bone f
+    ; strong_semiringmor_strong_mor :: StrongSetoid_Morphism f }.
 End morphism_classes.
 
 Section jections.
@@ -267,8 +267,8 @@ Section jections.
     ; surjective_mor : Setoid_Morphism f }.
 
   Class Bijective : Prop :=
-    { bijective_injective :> Injective
-    ; bijective_surjective :> Surjective }.
+    { bijective_injective :: Injective
+    ; bijective_surjective :: Surjective }.
 End jections.
 
 #[global]
diff --git a/interfaces/additional_operations.v b/interfaces/additional_operations.v
index a5c0c5b..7f454bb 100644
--- a/interfaces/additional_operations.v
+++ b/interfaces/additional_operations.v
@@ -34,7 +34,7 @@ Instance: Params (@shiftl) 3 := {}.
 
 Class ShiftLSpec A B (sl : ShiftL A B) `{Equiv A} `{Equiv B} `{One A} `{Plus A} `{Mult A} `{Zero B} `{One B} `{Plus B} := {
   shiftl_proper : Proper ((=) ==> (=) ==> (=)) (≪) ;
-  shiftl_0 :> RightIdentity (≪) 0 ;
+  shiftl_0 :: RightIdentity (≪) 0 ;
   shiftl_S : ∀ x n, x ≪ (1 + n) = 2 * x ≪ n
 }.
 
@@ -71,7 +71,7 @@ Instance: Params (@shiftr) 3 := {}.
 
 Class ShiftRSpec A B (sl : ShiftR A B) `{Equiv A} `{Equiv B} `{One A} `{Plus A} `{Mult A} `{Zero B} `{One B} `{Plus B} := {
   shiftr_proper : Proper ((=) ==> (=) ==> (=)) (≫) ;
-  shiftr_0 :> RightIdentity (≫) 0 ;
+  shiftr_0 :: RightIdentity (≫) 0 ;
   shiftr_S : ∀ x n, x ≫ n = 2 * x ≫ (1 + n) ∨ x ≫ n = 2 * x ≫ (1 + n) + 1
 }.
 
diff --git a/interfaces/canonical_names.v b/interfaces/canonical_names.v
index a41f2c9..bdd3449 100644
--- a/interfaces/canonical_names.v
+++ b/interfaces/canonical_names.v
@@ -405,12 +405,12 @@ Notation "f ⁻¹" := (inverse f) (at level 30) : mc_scope.
 Class Idempotent `{ea : Equiv A} (f: A → A → A) (x : A) : Prop := idempotency: f x x = x.
 Arguments idempotency {A ea} _ _ {Idempotent}.
 
-Class UnaryIdempotent `{Equiv A} (f: A → A) : Prop := unary_idempotent :> Idempotent (@compose A A A) f.
+Class UnaryIdempotent `{Equiv A} (f: A → A) : Prop := unary_idempotent :: Idempotent (@compose A A A) f.
 
 Lemma unary_idempotency `{Equiv A} `{!Reflexive (=)} `{!UnaryIdempotent f} x : f (f x) = f x.
 Proof. firstorder. Qed.
 
-Class BinaryIdempotent `{Equiv A} (op: A → A → A) : Prop := binary_idempotent :> ∀ x, Idempotent op x.
+Class BinaryIdempotent `{Equiv A} (op: A → A → A) : Prop := binary_idempotent :: ∀ x, Idempotent op x.
 
 Class LeftIdentity {A} `{Equiv B} (op : A → B → B) (x : A): Prop := left_identity: ∀ y, op x y = y.
 Class RightIdentity `{Equiv A} {B} (op : A → B → A) (y : B): Prop := right_identity: ∀ x, op x y = x.
@@ -428,7 +428,7 @@ Class Commutative `{Equiv B} `(f : A → A → B) : Prop := commutativity: ∀ x
 Class HeteroAssociative {A B C AB BC} `{Equiv ABC}
      (fA_BC: A → BC → ABC) (fBC: B → C → BC) (fAB_C: AB → C → ABC) (fAB : A → B → AB): Prop
    := associativity : ∀ x y z, fA_BC x (fBC y z) = fAB_C (fAB x y) z.
-Class Associative `{Equiv A} f := simple_associativity:> HeteroAssociative f f f f.
+Class Associative `{Equiv A} f := simple_associativity:: HeteroAssociative f f f f.
 Notation ArrowsAssociative C := (∀ {w x y z: C}, HeteroAssociative (◎) (comp z _ _ ) (◎) (comp y x w)).
 
 Class Involutive `{Equiv A} (f : A → A) := involutive: ∀ x, f (f x) = x.
@@ -451,8 +451,8 @@ Class LeftHeteroDistribute {A B} `{Equiv C} (f : A → B → C) (g_r : B → B 
   := distribute_l : ∀ a b c, f a (g_r b c) = g (f a b) (f a c).
 Class RightHeteroDistribute {A B} `{Equiv C} (f : A → B → C) (g_l : A → A → A) (g : C → C → C) : Prop
   := distribute_r: ∀ a b c, f (g_l a b) c = g (f a c) (f b c).
-Class LeftDistribute`{Equiv A} (f g: A → A → A) := simple_distribute_l :> LeftHeteroDistribute f g g.
-Class RightDistribute `{Equiv A} (f g: A → A → A) := simple_distribute_r :> RightHeteroDistribute f g g.
+Class LeftDistribute`{Equiv A} (f g: A → A → A) := simple_distribute_l :: LeftHeteroDistribute f g g.
+Class RightDistribute `{Equiv A} (f g: A → A → A) := simple_distribute_r :: RightHeteroDistribute f g g.
 
 Class HeteroSymmetric {A} {T : A → A → Type} (R : ∀ {x y}, T x y → T y x → Prop) : Prop :=
   hetero_symmetric `(a : T x y) (b : T y x) : R a b → R b a.
diff --git a/interfaces/finite_sets.v b/interfaces/finite_sets.v
index 2cda57e..a77b700 100644
--- a/interfaces/finite_sets.v
+++ b/interfaces/finite_sets.v
@@ -42,9 +42,9 @@ Class FSetExtend A `{t : SetType A} :=
 Class FSet A `{At : SetType A} `{Ae : Equiv A} `{Ate : SetEquiv A}
    `{Aempty : EmptySet A} `{Ajoin : SetJoin A} `{Asingle : SetSingleton A}
    `{∀ a₁ a₂ : A, Decision (a₁ = a₂)} `{U : !FSetExtend A} :=
- { fset_bounded_sl :> BoundedJoinSemiLattice (set_type A)
-  ; singleton_mor :> Setoid_Morphism singleton
-  ; fset_extend_mor `{BoundedJoinSemiLattice B} `{!Setoid_Morphism (f : A → B)} :>
+ { fset_bounded_sl :: BoundedJoinSemiLattice (set_type A)
+  ; singleton_mor :: Setoid_Morphism singleton
+  ; fset_extend_mor `{BoundedJoinSemiLattice B} `{!Setoid_Morphism (f : A → B)} ::
       BoundedJoinSemiLattice_Morphism (fset_extend f)
   ; fset_extend_correct `{BoundedJoinSemiLattice B}  (f : A → B) `{!Setoid_Morphism f} :
       f = fset_extend f ∘ singleton
@@ -63,7 +63,7 @@ freely use orders.lattices.alt_Build_JoinSemiLatticeOrder.
 
 Class FSetContainsSpec A `{At : SetType A} `{Ae : Equiv A} `{Ate : SetEquiv A}
      `{SetLe A} `{SetContains A} `{Ajoin : SetJoin A} `{Asingle : SetSingleton A} :=
-  { fset_join_sl_order :> JoinSemiLatticeOrder (≤)
+  { fset_join_sl_order :: JoinSemiLatticeOrder (≤)
   ; fset_in_singleton_le : ∀ x X, x ∈ X ↔ {{ x }} ≤ X }.
 
 (*
@@ -71,7 +71,7 @@ Unfortunately, properties as meet and the differences cannot be uniquely
 defined in an algebraic way, therefore we just use set inclusion.
 *)
 Class FullFSet A {car Ae conAe conAle Acontains Aempty Ajoin Asingle U Adec} `{Adiff : SetDifference A} `{Ameet : SetMeet A} :=
-  { full_fset_fset :> @FSet A car Ae conAe Aempty Ajoin Asingle U Adec
-  ; full_fset_contains :> @FSetContainsSpec A car Ae conAe conAle Acontains Ajoin Asingle
+  { full_fset_fset :: @FSet A car Ae conAe Aempty Ajoin Asingle U Adec
+  ; full_fset_contains :: @FSetContainsSpec A car Ae conAe conAle Acontains Ajoin Asingle
   ; fset_in_meet : ∀ X Y x, x ∈ X ⊓ Y ↔ (x ∈ X ∧ x ∈ Y)
   ; fset_in_difference : ∀ X Y x, x ∈ X∖ Y ↔ (x ∈ X ∧ x ∉ Y) }.
diff --git a/interfaces/functors.v b/interfaces/functors.v
index b7d1059..d5c7b4c 100644
--- a/interfaces/functors.v
+++ b/interfaces/functors.v
@@ -9,7 +9,7 @@ Section functor_class.
   Class Functor `(Fmap): Prop :=
     { functor_from: Category C
     ; functor_to: Category D
-    ; functor_morphism:> ∀ a b: C, Setoid_Morphism (@fmap _ a b)
+    ; functor_morphism:: ∀ a b: C, Setoid_Morphism (@fmap _ a b)
     ; preserves_id: `(fmap (cat_id: a ⟶ a) = cat_id)
     ; preserves_comp `(f: y ⟶ z) `(g: x ⟶ y): fmap (f ◎ g) = fmap f ◎ fmap g }.
 End functor_class.
@@ -123,8 +123,8 @@ Class SFmap (M : Type → Type) := sfmap: ∀ `(A → B), (M A → M B).
 
 Class SFunctor (M : Type → Type) 
      `{∀ `{Equiv A}, Equiv (M A)} `{SFmap M} : Prop :=
-  { sfunctor_setoid `{Setoid A} :> Setoid (M A)
-  ; sfmap_proper `{Setoid A} `{Setoid B} :>
+  { sfunctor_setoid `{Setoid A} :: Setoid (M A)
+  ; sfmap_proper `{Setoid A} `{Setoid B} ::
       Proper (((=) ==> (=)) ==> ((=) ==> (=))) (@sfmap M _ A B)
   ; sfmap_id `{Setoid A} : sfmap id = id
   ; sfmap_comp `{Equiv A} `{Equiv B} `{Equiv C} `{!Setoid_Morphism (f : B → C)} `{!Setoid_Morphism (g : A → B)} :
diff --git a/interfaces/integers.v b/interfaces/integers.v
index ae2208d..8a48888 100644
--- a/interfaces/integers.v
+++ b/interfaces/integers.v
@@ -33,9 +33,9 @@ End initial_maps.
 Instance: Params (@integers_to_ring) 8 := {}.
 
 Class Integers A {e plus mult zero one negate} `{U : IntegersToRing A} :=
-  { integers_ring:> @Ring A e plus mult zero one negate
-  ; integers_to_ring_mor:> ∀ `{Ring B}, SemiRing_Morphism (integers_to_ring A B)
-  ; integers_initial:> Initial (rings.object A) }.
+  { integers_ring:: @Ring A e plus mult zero one negate
+  ; integers_to_ring_mor:: ∀ `{Ring B}, SemiRing_Morphism (integers_to_ring A B)
+  ; integers_initial:: Initial (rings.object A) }.
 
 Section specializable.
   Context (Z N : Type) `{Integers Z} `{Naturals N}.
diff --git a/interfaces/monads.v b/interfaces/monads.v
index f6b637a..2716d90 100644
--- a/interfaces/monads.v
+++ b/interfaces/monads.v
@@ -21,10 +21,10 @@ Notation "x ← y ; z" := (y ≫= (λ x : _, z)) (at level 65, (*next at level 3
 
 Class Monad (M : Type → Type) `{∀ A, Equiv A → Equiv (M A)} 
      `{MonadReturn M} `{MonadBind M} : Prop :=
-  { mon_ret_proper `{Setoid A} :> Proper ((=) ==> (=)) (@ret _ _ A)
-  ; mon_bind_proper `{Setoid A} `{Setoid B} :>
+  { mon_ret_proper `{Setoid A} :: Proper ((=) ==> (=)) (@ret _ _ A)
+  ; mon_bind_proper `{Setoid A} `{Setoid B} ::
       Proper (((=) ==> (=)) ==> (=) ==> (=)) (@bind _ _ A B)
-  ; mon_setoid `{Setoid A} :> Setoid (M A)
+  ; mon_setoid `{Setoid A} :: Setoid (M A)
   ; bind_lunit `{Equiv A} `{Setoid B} `{!Setoid_Morphism (f : A → M B)} : bind f ∘ ret = f
   ; bind_runit `{Setoid A} : bind ret = id
   ; bind_assoc `{Equiv A} `{Equiv B} `{Setoid C} 
@@ -33,9 +33,9 @@ Class Monad (M : Type → Type) `{∀ A, Equiv A → Equiv (M A)}
 
 Class StrongMonad (M : Type → Type) `{∀ A, Equiv A → Equiv (M A)}
      `{MonadReturn M} `{SFmap M} `{MonadJoin M} : Prop :=
-  { smon_ret_proper `{Setoid A} :> Proper ((=) ==> (=)) (@ret _ _ A)
-  ; smon_join_proper `{Setoid A} :> Proper ((=) ==> (=)) (@join _ _ A)
-  ; smon_sfunctor :> SFunctor M  
+  { smon_ret_proper `{Setoid A} :: Proper ((=) ==> (=)) (@ret _ _ A)
+  ; smon_join_proper `{Setoid A} :: Proper ((=) ==> (=)) (@join _ _ A)
+  ; smon_sfunctor :: SFunctor M
   ; sfmap_ret `{Equiv A} `{Equiv B} `{!Setoid_Morphism (f : A → B)} :
       sfmap f ∘ ret = ret ∘ f
   ; sfmap_join `{Equiv A} `{Equiv B} `{!Setoid_Morphism (f : A → B)} : 
@@ -49,7 +49,7 @@ Class StrongMonad (M : Type → Type) `{∀ A, Equiv A → Equiv (M A)}
 
 Class FullMonad (M : Type → Type) `{∀ A, Equiv A → Equiv (M A)} 
      `{MonadReturn M} `{MonadBind M} `{SFmap M} `{MonadJoin M} : Prop := 
-  { full_mon_mon :> Monad M
-  ; full_smon :> StrongMonad M
+  { full_mon_mon :: Monad M
+  ; full_smon :: StrongMonad M
   ; bind_as_join_sfmap `{Equiv A} `{Setoid B} `{!Setoid_Morphism (f : A → M B)} :
       bind f = join ∘ sfmap f }.
diff --git a/interfaces/naturals.v b/interfaces/naturals.v
index 5c1befa..33d5f9f 100644
--- a/interfaces/naturals.v
+++ b/interfaces/naturals.v
@@ -4,7 +4,7 @@ Require Import
 
 Module bad.
   Class Naturals (A: semirings.Object) `{!InitialArrow A}: Prop :=
-    { naturals_initial:> Initial A }.
+    { naturals_initial:: Initial A }.
 End bad.
 
 Section initial_maps.
@@ -40,9 +40,9 @@ End initial_maps.
 Instance: Params (@naturals_to_semiring) 7 := {}.
 
 Class Naturals A {e plus mult zero one} `{U: NaturalsToSemiRing A} :=
-  { naturals_ring:> @SemiRing A e plus mult zero one
-  ; naturals_to_semiring_mor:> ∀ `{SemiRing B}, SemiRing_Morphism (naturals_to_semiring A B)
-  ; naturals_initial:> Initial (semirings.object A) }.
+  { naturals_ring:: @SemiRing A e plus mult zero one
+  ; naturals_to_semiring_mor:: ∀ `{SemiRing B}, SemiRing_Morphism (naturals_to_semiring A B)
+  ; naturals_initial:: Initial (semirings.object A) }.
 
 (* Specializable operations: *)
 Class NatDistance N `{Equiv N} `{Plus N}
diff --git a/interfaces/orders.v b/interfaces/orders.v
index c6598ec..826d3a2 100644
--- a/interfaces/orders.v
+++ b/interfaces/orders.v
@@ -19,13 +19,13 @@ usual properties like Trichotomy (<) and TotalRelation (≤).
 
 Class PartialOrder `{Ae : Equiv A} (Ale : Le A) : Prop :=
   { po_setoid : Setoid A (* Making this a subclass makes instance search slow *)
-  ; po_proper:> Proper ((=) ==> (=) ==> iff) (≤)
-  ; po_preorder:> PreOrder (≤)
-  ; po_antisym:> AntiSymmetric (≤) }.
+  ; po_proper:: Proper ((=) ==> (=) ==> iff) (≤)
+  ; po_preorder:: PreOrder (≤)
+  ; po_antisym:: AntiSymmetric (≤) }.
 
 Class TotalOrder `{Ae : Equiv A} (Ale : Le A) : Prop :=
-  { total_order_po :> PartialOrder (≤)
-  ; total_order_total :> TotalRelation (≤) }.
+  { total_order_po :: PartialOrder (≤)
+  ; total_order_total :: TotalRelation (≤) }.
 
 (*
 We define a variant of the order theoretic definition of meet and join
@@ -37,48 +37,48 @@ This is needed to prove equavalence with the algebraic definition. We
 do this in orders.lattices.
 *)
 Class MeetSemiLatticeOrder `{Ae : Equiv A} (Ale : Le A) `{Meet A} : Prop :=
-  { meet_sl_order :> PartialOrder (≤)
+  { meet_sl_order :: PartialOrder (≤)
   ; meet_lb_l : ∀ x y, x ⊓ y ≤ x
   ; meet_lb_r : ∀ x y, x ⊓ y ≤ y
   ; meet_glb : ∀ x y z, z ≤ x → z ≤ y → z ≤ x ⊓ y }.
 
 Class JoinSemiLatticeOrder `{Ae : Equiv A} (Ale : Le A) `{Join A} : Prop :=
-  { join_sl_order :> PartialOrder (≤)
+  { join_sl_order :: PartialOrder (≤)
   ; join_ub_l : ∀ x y, x ≤ x ⊔ y
   ; join_ub_r : ∀ x y, y ≤ x ⊔ y
   ; join_lub : ∀ x y z, x ≤ z → y ≤ z → x ⊔ y ≤ z }.
 
 Class LatticeOrder `{Ae : Equiv A} (Ale : Le A) `{Meet A} `{Join A} : Prop :=
-  { lattice_order_meet :> MeetSemiLatticeOrder (≤)
-  ; lattice_order_join :> JoinSemiLatticeOrder (≤) }.
+  { lattice_order_meet :: MeetSemiLatticeOrder (≤)
+  ; lattice_order_join :: JoinSemiLatticeOrder (≤) }.
 
 (* The strict order from the standard library does not include (=) and thus
   does not require (<) to be Proper. *)
 Class StrictSetoidOrder `{Ae : Equiv A} (Alt : Lt A) : Prop :=
   { strict_setoid_order_setoid : Setoid A
-  ; strict_setoid_order_proper :> Proper ((=) ==> (=) ==> iff) (<)
-  ; strict_setoid_order_strict :> StrictOrder (<) }.
+  ; strict_setoid_order_proper :: Proper ((=) ==> (=) ==> iff) (<)
+  ; strict_setoid_order_strict :: StrictOrder (<) }.
 
 (* The constructive notion of a total strict total order. Note that we get Proper (<)
   from cotransitivity. We will prove that (<) is in fact a StrictSetoidOrder. *)
 Class PseudoOrder `{Ae : Equiv A} `{Aap : Apart A} (Alt : Lt A) : Prop :=
   { pseudo_order_setoid : StrongSetoid A
   ; pseudo_order_antisym : ∀ x y, ¬(x < y ∧ y < x)
-  ; pseudo_order_cotrans :> CoTransitive (<)
+  ; pseudo_order_cotrans :: CoTransitive (<)
   ; apart_iff_total_lt : ∀ x y, x ≶ y ↔ x < y ∨ y < x }.
 
 (* A partial order (≤) with a corresponding (<). We will prove that (<) is in fact
   a StrictSetoidOrder *)
 Class FullPartialOrder `{Ae : Equiv A} `{Aap : Apart A} (Ale : Le A) (Alt : Lt A) : Prop :=
   { strict_po_setoid : StrongSetoid A
-  ; strict_po_po :> PartialOrder (≤)
-  ; strict_po_trans :> Transitive (<)
+  ; strict_po_po :: PartialOrder (≤)
+  ; strict_po_trans :: Transitive (<)
   ; lt_iff_le_apart : ∀ x y, x < y ↔ x ≤ y ∧ x ≶ y }.
 
 (* A pseudo order (<) with a corresponding (≤). We will prove that (≤) is in fact
   a PartialOrder. *)
 Class FullPseudoOrder `{Ae : Equiv A} `{Aap : Apart A} (Ale : Le A) (Alt : Lt A) : Prop :=
-  { full_pseudo_order_pseudo :> PseudoOrder Alt
+  { full_pseudo_order_pseudo :: PseudoOrder Alt
   ; le_iff_not_lt_flip : ∀ x y, x ≤ y ↔ ¬y < x }.
 
 Section order_maps.
@@ -97,32 +97,32 @@ Section order_maps.
     ; strict_order_morphism_so_b : StrictSetoidOrder Blt }.
 
   Class OrderPreserving :=
-    { order_preserving_morphism :> Order_Morphism
+    { order_preserving_morphism :: Order_Morphism
     ; order_preserving : `(x ≤ y → f x ≤ f y) }.
 
   Class OrderReflecting :=
-    { order_reflecting_morphism :> Order_Morphism
+    { order_reflecting_morphism :: Order_Morphism
     ; order_reflecting : `(f x ≤ f y → x ≤ y) }.
 
   Class OrderEmbedding :=
-    { order_embedding_preserving :> OrderPreserving
-    ; order_embedding_reflecting :> OrderReflecting }.
+    { order_embedding_preserving :: OrderPreserving
+    ; order_embedding_reflecting :: OrderReflecting }.
 
   Class OrderIsomorphism `{!Inverse f} :=
-    { order_iso_embedding :> OrderEmbedding
-    ; order_iso_surjective :> Surjective f }.
+    { order_iso_embedding :: OrderEmbedding
+    ; order_iso_surjective :: Surjective f }.
 
   Class StrictlyOrderPreserving :=
-    { strictly_order_preserving_morphism :> StrictOrder_Morphism
+    { strictly_order_preserving_morphism :: StrictOrder_Morphism
     ; strictly_order_preserving : `(x < y → f x < f y) }.
 
   Class StrictlyOrderReflecting :=
-    { strictly_order_reflecting_morphism :> StrictOrder_Morphism
+    { strictly_order_reflecting_morphism :: StrictOrder_Morphism
     ; strictly_order_reflecting : `(f x < f y → x < y) }.
 
   Class StrictOrderEmbedding :=
-    { strict_order_embedding_preserving :> StrictlyOrderPreserving
-    ; strict_order_embedding_reflecting :> StrictlyOrderReflecting }.
+    { strict_order_embedding_preserving :: StrictlyOrderPreserving
+    ; strict_order_embedding_reflecting :: StrictlyOrderReflecting }.
 End order_maps.
 
 #[global]
@@ -139,32 +139,32 @@ Davorin Lešnik's PhD thesis.
 *)
 Class SemiRingOrder `{Equiv A} `{Plus A} `{Mult A}
     `{Zero A} `{One A} (Ale : Le A) :=
-  { srorder_po :> PartialOrder Ale
+  { srorder_po :: PartialOrder Ale
   ; srorder_semiring : SemiRing A
   ; srorder_partial_minus : ∀ x y, x ≤ y → ∃ z, y = x + z
-  ; srorder_plus :> ∀ z, OrderEmbedding (z +)
+  ; srorder_plus :: ∀ z, OrderEmbedding (z +)
   ; nonneg_mult_compat : ∀ x y, PropHolds (0 ≤ x) → PropHolds (0 ≤ y) → PropHolds (0 ≤ x * y) }.
 
 Class StrictSemiRingOrder `{Equiv A} `{Plus A} `{Mult A}
     `{Zero A} `{One A} (Alt : Lt A) :=
-  { strict_srorder_so :> StrictSetoidOrder Alt
+  { strict_srorder_so :: StrictSetoidOrder Alt
   ; strict_srorder_semiring : SemiRing A
   ; strict_srorder_partial_minus : ∀ x y, x < y → ∃ z, y = x + z
-  ; strict_srorder_plus :> ∀ z, StrictOrderEmbedding (z +)
+  ; strict_srorder_plus :: ∀ z, StrictOrderEmbedding (z +)
   ; pos_mult_compat : ∀ x y, PropHolds (0 < x) → PropHolds (0 < y) → PropHolds (0 < x * y) }.
 
 Class PseudoSemiRingOrder `{Equiv A} `{Apart A} `{Plus A}
     `{Mult A} `{Zero A} `{One A} (Alt : Lt A) :=
-  { pseudo_srorder_strict :> PseudoOrder Alt
+  { pseudo_srorder_strict :: PseudoOrder Alt
   ; pseudo_srorder_semiring : SemiRing A
   ; pseudo_srorder_partial_minus : ∀ x y, ¬y < x → ∃ z, y = x + z
-  ; pseudo_srorder_plus :> ∀ z, StrictOrderEmbedding (z +)
-  ; pseudo_srorder_mult_ext :> StrongSetoid_BinaryMorphism (.*.)
+  ; pseudo_srorder_plus :: ∀ z, StrictOrderEmbedding (z +)
+  ; pseudo_srorder_mult_ext :: StrongSetoid_BinaryMorphism (.*.)
   ; pseudo_srorder_pos_mult_compat : ∀ x y, PropHolds (0 < x) → PropHolds (0 < y) → PropHolds (0 < x * y) }.
 
 Class FullPseudoSemiRingOrder `{Equiv A} `{Apart A} `{Plus A}
     `{Mult A} `{Zero A} `{One A} (Ale : Le A) (Alt : Lt A) :=
-  { full_pseudo_srorder_pso :> PseudoSemiRingOrder Alt
+  { full_pseudo_srorder_pso :: PseudoSemiRingOrder Alt
   ; full_pseudo_srorder_le_iff_not_lt_flip : ∀ x y, x ≤ y ↔ ¬y < x }.
 
 (* Due to bug #2528 *)
@@ -177,8 +177,8 @@ Hint Extern 7 (PropHolds (0 ≤ _ * _)) => eapply @nonneg_mult_compat : typeclas
 Alternatively, we could have defined the standard notion of a RingOrder:
 
 Class RingOrder `{Equiv A} `{Plus A} `{Mult A} `{Zero A} (Ale : Le A) :=
-  { ringorder_po :> PartialOrder Ale
-  ; ringorder_plus :> ∀ z, OrderPreserving (z +)
+  { ringorder_po :: PartialOrder Ale
+  ; ringorder_plus :: ∀ z, OrderPreserving (z +)
   ; ringorder_mult : ∀ x y, 0 ≤ x → 0 ≤ y → 0 ≤ x * y }.
 
 Unfortunately, this notion is too weak when we consider semirings (e.g. the
@@ -190,8 +190,8 @@ Similarly we prove that a FullSemiRingOrder and a FullPseudoRingOrder are equiva
 
 Class FullPseudoRingOrder `{Equiv A} `{Apart A} `{Plus A}
     `{Mult A} `{Zero A} (Ale : Le A) (Alt : Lt A) :=
-  { pseudo_ringorder_spo :> FullPseudoOrder Ale Alt
-  ; pseudo_ringorder_mult_ext :> StrongSetoid_BinaryMorphism (.*.)
-  ; pseudo_ringorder_plus :> ∀ z, StrictlyOrderPreserving (z +)
+  { pseudo_ringorder_spo :: FullPseudoOrder Ale Alt
+  ; pseudo_ringorder_mult_ext :: StrongSetoid_BinaryMorphism (.*.)
+  ; pseudo_ringorder_plus :: ∀ z, StrictlyOrderPreserving (z +)
   ; pseudo_ringorder_mult : ∀ x y, 0 < x → 0 < y → 0 < x * y }.
 *)
diff --git a/interfaces/rationals.v b/interfaces/rationals.v
index 3298895..afcdf29 100644
--- a/interfaces/rationals.v
+++ b/interfaces/rationals.v
@@ -18,7 +18,7 @@ implementation of the integers.
 *)
 
 Class Rationals A {e plus mult zero one neg recip} `{U : !RationalsToFrac A} : Prop :=
-  { rationals_field:> @DecField A e plus mult zero one neg recip
-  ; rationals_frac :> ∀ `{Integers Z}, Injective (rationals_to_frac A Z)
-  ; rationals_frac_mor :> ∀ `{Integers Z}, SemiRing_Morphism (rationals_to_frac A Z)
-  ; rationals_embed_ints :> ∀ `{Integers Z}, Injective (integers_to_ring Z A) }.
+  { rationals_field:: @DecField A e plus mult zero one neg recip
+  ; rationals_frac :: ∀ `{Integers Z}, Injective (rationals_to_frac A Z)
+  ; rationals_frac_mor :: ∀ `{Integers Z}, SemiRing_Morphism (rationals_to_frac A Z)
+  ; rationals_embed_ints :: ∀ `{Integers Z}, Injective (integers_to_ring Z A) }.
diff --git a/interfaces/sequences.v b/interfaces/sequences.v
index 720ea29..1829c89 100644
--- a/interfaces/sequences.v
+++ b/interfaces/sequences.v
@@ -44,15 +44,15 @@ Section practical.
    `{!InjectToSeq free} `{!ExtendToSeq free}.
 
   Class Sequence :=
-    { sequence_makes_monoids:> ∀ `{Setoid a}, Monoid (free a)
-    ; sequence_inject_morphism:> ∀ `{Setoid a}, Setoid_Morphism (inject a)
-    ; sequence_map_morphism:> ∀ `{Equiv x} `{Equiv y} (f: x → y),
+    { sequence_makes_monoids:: ∀ `{Setoid a}, Monoid (free a)
+    ; sequence_inject_morphism:: ∀ `{Setoid a}, Setoid_Morphism (inject a)
+    ; sequence_map_morphism:: ∀ `{Equiv x} `{Equiv y} (f: x → y),
         Setoid_Morphism f → Monoid_Morphism (raw_fmap _ _ f)
     ; sequence_fmap_proper: ∀ `{Equiv x} `{Equiv y} (f g: x → y), f = g → fmap free f = raw_fmap _ _ g
     ; sequence_fmap_id: ∀ `{Equiv x}, raw_fmap _ _ (@id x) = id
     ; sequence_fmap_comp: ∀ `{Equiv x} `{Equiv y} `{Equiv z} (f: y → z) (g: x → y),
         raw_fmap _ _ (f ∘ g) = raw_fmap _ _ f ∘ raw_fmap _ _ g
-    ; sequence_extend_makes_morphisms:> ∀ `{Equiv x} `{Monoid y} (f: x → y),
+    ; sequence_extend_makes_morphisms:: ∀ `{Equiv x} `{Monoid y} (f: x → y),
         Setoid_Morphism f → Monoid_Morphism (extend f)
     ; sequence_inject_natural: ∀ `{Setoid A} `{Setoid B} (f: A → B), Setoid_Morphism f →
         inject B ∘ f = raw_fmap _ _ f ∘ inject A
diff --git a/interfaces/ua_basic.v b/interfaces/ua_basic.v
index 6281d0a..b78463e 100644
--- a/interfaces/ua_basic.v
+++ b/interfaces/ua_basic.v
@@ -106,5 +106,5 @@ Class Algebra
   (carriers: sorts σ → Type)
   {e: ∀ a, Equiv (carriers a)}
   `{AlgebraOps σ carriers}: Prop :=
-    { algebra_setoids:> ∀ a, Setoid (carriers a)
-    ; algebra_propers:> ∀ o: σ, Proper (=) (algebra_op o) }.
+    { algebra_setoids:: ∀ a, Setoid (carriers a)
+    ; algebra_propers:: ∀ o: σ, Proper (=) (algebra_op o) }.
diff --git a/interfaces/universal_algebra.v b/interfaces/universal_algebra.v
index 00af0bf..6701992 100644
--- a/interfaces/universal_algebra.v
+++ b/interfaces/universal_algebra.v
@@ -265,7 +265,7 @@ Class InVariety
   (carriers: sorts et → Type)
   {e: ∀ a, Equiv (carriers a)}
   `{!AlgebraOps et carriers}: Prop :=
-  { variety_algebra:> Algebra et carriers
+  { variety_algebra:: Algebra et carriers
   ; variety_laws: ∀ s, et_laws et s → ∀ vars, eval_stmt et vars s }.
 
 Module op_type_notations.
diff --git a/interfaces/vectorspace.v b/interfaces/vectorspace.v
index 2d8c1f8..038e363 100644
--- a/interfaces/vectorspace.v
+++ b/interfaces/vectorspace.v
@@ -36,13 +36,13 @@ Class Module (R M : Type)
   {Me Mop Munit Mnegate}
   {sm : ScalarMult R M}
 :=
-  { lm_ring            :> @Ring R Re Rplus Rmult Rzero Rone Rnegate
-  ; lm_group           :> @AbGroup M Me Mop Munit Mnegate
-  ; lm_distr_l         :> LeftHeteroDistribute (·) (&) (&)
-  ; lm_distr_r         :> RightHeteroDistribute (·) (+) (&)
-  ; lm_assoc           :> HeteroAssociative (·) (·) (·) (.*.)
-  ; lm_identity        :> LeftIdentity (·) 1
-  ; scalar_mult_proper :> Proper ((=) ==> (=) ==> (=)) sm
+  { lm_ring            :: @Ring R Re Rplus Rmult Rzero Rone Rnegate
+  ; lm_group           :: @AbGroup M Me Mop Munit Mnegate
+  ; lm_distr_l         :: LeftHeteroDistribute (·) (&) (&)
+  ; lm_distr_r         :: RightHeteroDistribute (·) (+) (&)
+  ; lm_assoc           :: HeteroAssociative (·) (·) (·) (.*.)
+  ; lm_identity        :: LeftIdentity (·) 1
+  ; scalar_mult_proper :: Proper ((=) ==> (=) ==> (=)) sm
   }.
 
 (* TODO K is commutative, so derive right module laws? *)
@@ -54,9 +54,9 @@ Class Seminormed
  `{!Abs R} (n : Norm R M)
 :=
   (* We have a module *)
-  { snm_module      :> @Module R M Re Rplus Rmult Rzero Rone Rnegate
+  { snm_module      :: @Module R M Re Rplus Rmult Rzero Rone Rnegate
                                   Me Mop Munit Mnegate Smult
-  ; snm_order       :> @FullPseudoSemiRingOrder R Re Rapart Rplus Rmult Rzero Rone Rle Rlt
+  ; snm_order       :: @FullPseudoSemiRingOrder R Re Rapart Rplus Rmult Rzero Rone Rle Rlt
 
   (* With respect to which our norm preserves the following: *)
   ; snm_scale       :  ∀ a v, ∥a · v∥ = (abs a) * ∥v∥   (* positive homgeneity *)
@@ -73,9 +73,9 @@ Class VectorSpace (K V : Type)
    {Ve Vop Vunit Vnegate}                     (* vector operations *)
    {sm : ScalarMult K V}
  :=
-   { vs_field         :> @DecField K Ke Kplus Kmult Kzero Kone Knegate Krecip
-   ; vs_abgroup       :> @AbGroup V Ve Vop Vunit Vnegate
-   ; vs_module        :> @Module K V Ke Kplus Kmult Kzero Kone Knegate
+   { vs_field         :: @DecField K Ke Kplus Kmult Kzero Kone Knegate Krecip
+   ; vs_abgroup       :: @AbGroup V Ve Vop Vunit Vnegate
+   ; vs_module        :: @Module K V Ke Kplus Kmult Kzero Kone Knegate
                                       Ve Vop Vunit Vnegate sm
    }.
 
@@ -87,14 +87,14 @@ Class InnerProductSpace (K V : Type)
    {Ve Vop Vunit Vnegate}                     (* vector operations *)
    {sm : ScalarMult K V} {inp: Inproduct K V} {Kle: Le K}
  :=
-   { in_vectorspace   :> @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate
+   { in_vectorspace   :: @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate
                                       Krecip Ve Vop Vunit Vnegate sm
-   ; in_srorder       :> SemiRingOrder Kle
-   ; in_comm          :> Commutative inprod
+   ; in_srorder       :: SemiRingOrder Kle
+   ; in_comm          :: Commutative inprod
    ; in_linear_l      :  ∀ a u v, ⟨a·u,v⟩ = a*⟨u,v⟩
-   ; in_nonneg        :> ∀ v, PropHolds (0 ≤ ⟨v,v⟩) (* TODO Le to strong? *)
-   ; in_mon_unit_zero :> ∀ v, 0 = ⟨v,v⟩ <-> v = mon_unit
-   ; inprod_proper    :> Proper ((=) ==> (=) ==> (=)) (⟨⟩)
+   ; in_nonneg        :: ∀ v, PropHolds (0 ≤ ⟨v,v⟩) (* TODO Le to strong? *)
+   ; in_mon_unit_zero :: ∀ v, 0 = ⟨v,v⟩ <-> v = mon_unit
+   ; inprod_proper    :: Proper ((=) ==> (=) ==> (=)) (⟨⟩)
    }.
 
 (* TODO complex conjugate?
@@ -115,7 +115,7 @@ Class SemiNormedSpace (K V : Type)
    {Ve Vop Vunit Vnegate}                     (* vector operations *)
    {sm : ScalarMult K V}
  :=
-   { sn_vectorspace :> @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate
+   { sn_vectorspace :: @VectorSpace K V Ke Kplus Kmult Kzero Kone Knegate
                                     Krecip Ve Vop Vunit Vnegate sm
    ; sn_nonneg      :  ∀ v, 0 ≤ ∥v∥                     (* non-negativity *)
    ; sn_scale       :  ∀ a v, ∥a · v∥ = (abs a) * ∥v∥   (* positive homgeneity *)
diff --git a/meta.yml b/meta.yml
index 06487b6..bd0d312 100644
--- a/meta.yml
+++ b/meta.yml
@@ -49,19 +49,13 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: Coq 8.11 or later (use releases for other Coq versions)
-  opam: '{(>= "8.11" & < "8.19~") | (= "dev")}'
+  text: Coq 8.18 or later (use releases for other Coq versions)
+  opam: '{(>= "8.18" & < "8.20~") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: dev
+- version: "8.19"
 - version: "8.18"
-- version: "8.17"
-- version: "8.16"
-- version: "8.15"
-- version: "8.14"
-- version: "8.13"
-- version: "8.12"
-- version: "8.11"
 
 dependencies:
 - opam:
diff --git a/theory/forget_variety.v b/theory/forget_variety.v
index 8fdd413..37f5068 100644
--- a/theory/forget_variety.v
+++ b/theory/forget_variety.v
@@ -1,7 +1,7 @@
 (* "Forgetting" a variety's laws (but keeping the algebraic operations) is a trivial functor. *)
 
 Require Import
-  MathClasses.interfaces.canonical_names MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors
+  MathClasses.interfaces.canonical_names MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors
   MathClasses.theory.categories MathClasses.categories.varieties MathClasses.categories.algebras.
 
 Section contents.
diff --git a/theory/ring_ideals.v b/theory/ring_ideals.v
index 2938f67..cd5ecff 100644
--- a/theory/ring_ideals.v
+++ b/theory/ring_ideals.v
@@ -8,8 +8,8 @@ Require Export
 (* Require ua_congruence varieties.rings. *)
 
 Class RingIdeal A (P : A → Prop) `{Ring A} : Prop :=
-  { ideal_proper :> Proper ((=) ==> iff) P
-  ; ideal_NonEmpty :> NonEmpty (sig P)
+  { ideal_proper :: Proper ((=) ==> iff) P
+  ; ideal_NonEmpty :: NonEmpty (sig P)
   ; ideal_closed_plus_negate : ∀ x y, P x → P y → P (x - y)
   ; ideal_closed_mult_r : ∀ x y, P x → P (x * y)
   ; ideal_closed_mult_l: ∀ x y, P y → P (x * y) }.
diff --git a/theory/ua_congruence.v b/theory/ua_congruence.v
index ecbf24f..7b84c43 100644
--- a/theory/ua_congruence.v
+++ b/theory/ua_congruence.v
@@ -1,6 +1,6 @@
 Require Import
   Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List
-  MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebraT MathClasses.misc.util.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebraT MathClasses.misc.util.
 Require MathClasses.theory.ua_products.
 
 Require MathClasses.theory.categories.
@@ -121,8 +121,8 @@ Section contents.
   (* This justifies the following definition of a congruence: *)
 
   Class Congruence: Prop :=
-    { congruence_proper:> ∀ s: sorts σ, Proper ((=) ==> (=) ==> iff) (e s)
-    ; congruence_quotient:> Algebra σ v (e:=e) }.
+    { congruence_proper:: ∀ s: sorts σ, Proper ((=) ==> (=) ==> iff) (e s)
+    ; congruence_quotient:: Algebra σ v (e:=e) }.
 
 End contents.
 
diff --git a/theory/ua_homomorphisms.v b/theory/ua_homomorphisms.v
index 2f45671..7b527bd 100644
--- a/theory/ua_homomorphisms.v
+++ b/theory/ua_homomorphisms.v
@@ -23,7 +23,7 @@ Section contents.
       end.
 
     Class HomoMorphism: Prop :=
-      { homo_proper:> ∀ a, Setoid_Morphism (@f a)
+      { homo_proper:: ∀ a, Setoid_Morphism (@f a)
       ; preserves: ∀ (o: σ), Preservation (A_ops o) (B_ops o)
       ; homo_source_algebra: Algebra σ A
       ; homo_target_algebra: Algebra σ B }.
diff --git a/theory/ua_subalgebra.v b/theory/ua_subalgebra.v
index 130185a..93c5736 100644
--- a/theory/ua_subalgebra.v
+++ b/theory/ua_subalgebra.v
@@ -25,7 +25,7 @@ Section subalgebras.
   Qed.
 
   Class ClosedSubset: Prop :=
-    { subset_proper:> ∀ s, Proper ((=) ==> iff) (P s)
+    { subset_proper:: ∀ s, Proper ((=) ==> iff) (P s)
     ; subset_closed: ∀ o, op_closed (algebra_op o) }.
 
   (* Now suppose P is closed in this way. *)
diff --git a/theory/ua_subvariety.v b/theory/ua_subvariety.v
index d135add..48045dc 100644
--- a/theory/ua_subvariety.v
+++ b/theory/ua_subvariety.v
@@ -1,6 +1,6 @@
 Require Import
   Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Program.Program
-  MathClasses.interfaces.universal_algebra MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebra.
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebra.
 
 (* In theory/ua_subalgebra.v we defined closed proper subsets and showed that
 they yield subalgebras. We now expand on this result and show that they