Merge PR #18590: Uniformize semantics of :> in class after deprecatio…

…n phase of #16230 Reviewed-by: SkySkimmer Ack-by: JasonGross Co-authored-by: SkySkimmer <[email protected]>
coq · Mar 15, 2024 · a091b25 · a091b25
2 parents 4c3f2e2 + 55b5f53
commit a091b25
Show file tree

Hide file tree

Showing 47 changed files with 141 additions and 101 deletions.
diff --git a/doc/changelog/02-specification-language/18590-cleanup_16230.rst b/doc/changelog/02-specification-language/18590-cleanup_16230.rst
@@ -0,0 +1,51 @@
+- **Changed:**
+  warnings `future-coercion-class-constructor`
+  and `future-coercion-class-field` about ``:>`` in :cmd:`Class` as
+  error by default. This offers a last opportunity to replace ``:>``
+  with ``::`` (available since Coq 8.18) to declare typeclass instances
+  before making ``:>`` consistently declare coercions in all records in
+  next version.
+  To adapt huge codebases, you can try
+  `this script <https://gist.github.com/JasonGross/59fc3c03664f2280849abf50b531be42>`_
+  or the one below. But beware that both are incomplete.
+
+  .. code-block:: sh
+
+     #!/bin/awk -f
+     BEGIN {
+       startclass = 0;
+       inclass = 0;
+       indefclass = 0;  # definitionalclasses (single field, without { ... })
+     }
+     {
+       if ($0 ~ "[ ]*Class") {
+         startclass = 1;
+       }
+       if (startclass == 1 && $0 ~ ":=") {
+         inclass = 1;
+         indefclass = 1;
+       }
+       if (startclass == 1 && $0 ~ ":=.*{") {
+         indefclass = 0;
+       }
+       if (inclass == 1) startclass = 0;
+
+       if (inclass == 1 && $0 ~ ":>") {
+         if ($0 ~ "{ .*:>") {  # first field on a single line
+           sub("{ ", "{ #[global] ");
+         } else if ($0 ~ ":=.*:>") {  # definitional classes on a single line
+           sub(":= ", ":= #[global] ");
+         } else if ($0 ~ "^  ") {
+           sub("  ", "  #[global] ");
+         } else {
+           $0 = "#[global] " $0;
+         }
+         sub(":>", "::")
+       }
+     print $0;
+
+     if ($0 ~ ".*}[.]" || indefclass == 1 && $0 ~ "[.]$") inclass = 0;
+   }
+
+  (`#18590 <https://github.com/coq/coq/pull/18590>`_,
+  by Pierre Roux).
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
@@ -248,7 +248,7 @@ the implicit arguments mechanism if available, as shown in the example.
 Substructures
 ~~~~~~~~~~~~~
 
-.. index:: :> (substructure)
+.. index:: :: (substructure)
 
 Substructures are components of a typeclass which are themselves instances of a
 typeclass. They often arise when using typeclasses for logical properties, e.g.:

diff --git a/test-suite/bugs/HoTT_coq_058.v b/test-suite/bugs/HoTT_coq_058.v
@@ -30,7 +30,7 @@ Local Open Scope equiv_scope.
 
 Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
 
-Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+Class Funext := { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
 
 Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
   (forall x, f x = g x) -> f = g

diff --git a/test-suite/bugs/HoTT_coq_059.v b/test-suite/bugs/HoTT_coq_059.v
@@ -5,7 +5,7 @@ Inductive eq {A} (x : A) : A -> Type := eq_refl : eq x x.
 Notation "a = b" := (eq a b) : type_scope.
 
 Section foo.
-  Class Funext := { path_forall :> forall A P (f g : forall x : A, P x), (forall x, f x = g x) -> f = g }.
+  Class Funext := { path_forall :: forall A P (f g : forall x : A, P x), (forall x, f x = g x) -> f = g }.
   Context `{Funext, Funext}.
 
   Set Printing Universes.

diff --git a/test-suite/bugs/HoTT_coq_062.v b/test-suite/bugs/HoTT_coq_062.v
@@ -52,7 +52,7 @@ Definition equiv_path (A B : Type) (p : A = B) : A <~> B
   := BuildEquiv _ _ (transport (fun X:Type => X) p) admit.
 
 Class Univalence :=
-  isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B) .
+  isequiv_equiv_path :: forall (A B : Type), IsEquiv (equiv_path A B) .
 
 Section Univalence.
   Context `{Univalence}.

diff --git a/test-suite/bugs/HoTT_coq_088.v b/test-suite/bugs/HoTT_coq_088.v
@@ -35,7 +35,7 @@ Definition equiv_path (A B : Type) (p : A = B) : Equiv A B.
 Admitted.
 
 Class Univalence := {
-  isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
+  isequiv_equiv_path :: forall (A B : Type), IsEquiv (equiv_path A B)
 }.
 
 Definition ua_downward_closed `{Univalence} : Univalence.

diff --git a/test-suite/bugs/HoTT_coq_108.v b/test-suite/bugs/HoTT_coq_108.v
@@ -61,7 +61,7 @@ Notation Contr := (IsTrunc minus_two).
 Notation IsHSet := (IsTrunc 0).
 
 Class Funext :=
-  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+  { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
 Global Instance contr_forall `{Funext} `{P : A -> Type} `{forall a, Contr (P a)}
 : Contr (forall a, P a) | 100.
 admit.

diff --git a/test-suite/bugs/HoTT_coq_112.v b/test-suite/bugs/HoTT_coq_112.v
@@ -42,7 +42,7 @@ Definition equiv_path (A B : Type) (p : A = B) : A <~> B
   := BuildEquiv _ _ (transport (fun X:Type => X) p) _.
 
 Class Univalence := {
-  isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
+  isequiv_equiv_path :: forall (A B : Type), IsEquiv (equiv_path A B)
 }.
 
 Section Univalence.

diff --git a/test-suite/bugs/HoTT_coq_123.v b/test-suite/bugs/HoTT_coq_123.v
@@ -46,7 +46,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type :=
 Notation IsHSet := (IsTrunc minus_two).
 
 Class Funext :=
-  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+  { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
 
 Local Open Scope equiv_scope.
 

diff --git a/test-suite/bugs/bug_14221.v b/test-suite/bugs/bug_14221.v
@@ -14,7 +14,7 @@ Notation "∀  x .. y , P" := (forall x, .. (forall y, P) ..)
 
 Class Setoid A := {
   equiv : crelation A;
-  setoid_equiv :> Equivalence equiv
+  setoid_equiv :: Equivalence equiv
 }.
 
 Notation "f ≈ g" := (equiv f g) (at level 79).
@@ -46,7 +46,7 @@ Class Category := {
 
   uhom := Type : Type;
   hom : obj -> obj -> uhom where "a ~> b" := (hom a b);
-  homset :> ∀ X Y, Setoid (X ~> Y);
+  homset :: ∀ X Y, Setoid (X ~> Y);
 
   id {x} : x ~> x;
 }.
@@ -71,7 +71,7 @@ Class Functor (C D : Category) := {
   fobj : C -> D;
   fmap {x y : C} (f : x ~> y) : fobj x ~> fobj y;
 
-  fmap_respects :> ∀ x y, Proper (equiv ==> equiv) (@fmap x y);
+  fmap_respects :: ∀ x y, Proper (equiv ==> equiv) (@fmap x y);
 
   fmap_id {x : C} : fmap (@id C x) ≈ id;
 }.

diff --git a/test-suite/bugs/bug_15099.v b/test-suite/bugs/bug_15099.v
@@ -8,7 +8,7 @@ Set Universe Polymorphism.
 
 Class Setoid A := {
   equiv : crelation A;
-  setoid_equiv :> Equivalence equiv
+  setoid_equiv :: Equivalence equiv
 }.
 
 Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope.
@@ -19,7 +19,7 @@ Class Category := {
   obj : Type;
 
   hom : obj -> obj -> Type where "a ~> b" := (hom a b);
-  homset :> forall X Y, Setoid (X ~> Y);
+  homset :: forall X Y, Setoid (X ~> Y);
 
   id {x} : x ~> x;
 
@@ -38,7 +38,7 @@ Class Functor {C D : Category} := {
   fobj : C -> D;
   fmap {x y : C} (f : x ~> y) : fobj x ~> fobj y;
 
-  fmap_respects :> forall x y, Proper (equiv ==> equiv) (@fmap x y);
+  fmap_respects :: forall x y, Proper (equiv ==> equiv) (@fmap x y);
 
   fmap_id {x : C} : fmap (@id C x) ≈ id;
 }.

diff --git a/test-suite/bugs/bug_16204.v b/test-suite/bugs/bug_16204.v
@@ -6,7 +6,7 @@ Class IsProp (A : Type) : Prop :=
   irrel (x y : A) : x = y.
 
 Class IsProofIrrel : Prop :=
-  proof_irrel (A : Prop) :> IsProp A.
+  proof_irrel (A : Prop) :: IsProp A.
 
 Class IsPropExt : Prop :=
   prop_ext (A B : Prop) (a : A <-> B) : A = B.

diff --git a/test-suite/bugs/bug_3321.v b/test-suite/bugs/bug_3321.v
@@ -7,7 +7,7 @@ Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A ; e
 Record Equiv A B := BuildEquiv { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }.
 Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
 Definition equiv_path (A B : Type) (p : A = B) : Equiv A B := admit.
-Class Univalence := { isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B) }.
+Class Univalence := { isequiv_equiv_path :: forall (A B : Type), IsEquiv (equiv_path A B) }.
 Definition path_universe `{Univalence} {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B) := admit.
 Context `{ua:Univalence}.
 Variable A:Type.

diff --git a/test-suite/bugs/bug_3329.v b/test-suite/bugs/bug_3329.v
@@ -15,7 +15,7 @@ Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
   := fun x => match h with idpath => idpath end.
 Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
 Class IsHSet (A : Type) := { _ : False }.
-Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+Class Funext := { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
 Record PreCategory :=
   { object :> Type;
     morphism : object -> object -> Type;

diff --git a/test-suite/bugs/bug_3330.v b/test-suite/bugs/bug_3330.v
@@ -132,7 +132,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type :=
 Notation IsHSet := (IsTrunc 0).
 
 Class Funext :=
-  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+  { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
 
 Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
   f == g -> f = g
@@ -357,8 +357,8 @@ Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) :=
 
 Class Isomorphic {C : PreCategory} s d :=
   {
-    morphism_isomorphic :> morphism C s d;
-    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
+    morphism_isomorphic :: morphism C s d;
+    isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic
   }.
 
 Module Export CategoryMorphismsNotations.

diff --git a/test-suite/bugs/bug_3393.v b/test-suite/bugs/bug_3393.v
@@ -13,7 +13,7 @@ Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
 Delimit Scope equiv_scope with equiv.
 Local Open Scope equiv_scope.
 Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
-Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+Class Funext := { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
 Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) : (forall x, f x = g x) -> f = g := (@apD10 A P f g)^-1.
 Record PreCategory :=
   { object :> Type;
@@ -33,8 +33,8 @@ Notation "F '_1' m" := (@morphism_of _ _ F _ _ m) (at level 10, no associativity
 Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }.
 Local Notation "m ^-1" := (morphism_inverse (m := m)) : morphism_scope.
 Class Isomorphic {C : PreCategory} s d :=
-  { morphism_isomorphic :> morphism C s d;
-    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+  { morphism_isomorphic :: morphism C s d;
+    isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic }.
 Coercion morphism_isomorphic : Isomorphic >-> morphism.
 Definition isisomorphism_inverse `(@IsIsomorphism C x y m) : IsIsomorphism m^-1 := {| morphism_inverse := m |}.
 

diff --git a/test-suite/bugs/bug_3422.v b/test-suite/bugs/bug_3422.v
@@ -52,8 +52,8 @@ Local Notation "m ^-1" := (morphism_inverse (m := m)) : morphism_scope.
 
 Class Isomorphic {C : PreCategory} s d :=
   {
-    morphism_isomorphic :> morphism C s d;
-    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
+    morphism_isomorphic :: morphism C s d;
+    isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic
   }.
 
 Coercion morphism_isomorphic : Isomorphic >-> morphism.

diff --git a/test-suite/bugs/bug_3427.v b/test-suite/bugs/bug_3427.v
@@ -74,7 +74,7 @@ Notation IsHProp := (IsTrunc minus_one).
 Notation IsHSet := (IsTrunc 0).
 
 Class Funext :=
-  { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+  { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
 
 Definition concat_pV {A : Type} {x y : A} (p : x = y) :
   p @ p^ = 1
@@ -136,7 +136,7 @@ Definition equiv_path (A B : Type) (p : A = B) : A <~> B
   := BuildEquiv _ _ (transport (fun X:Type => X) p) _.
 
 Class Univalence := {
-                     isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
+                     isequiv_equiv_path :: forall (A B : Type), IsEquiv (equiv_path A B)
                    }.
 
 Section Univalence.

diff --git a/test-suite/bugs/bug_3480.v b/test-suite/bugs/bug_3480.v
@@ -10,7 +10,7 @@ Delimit Scope category_scope with category.
 Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
 Local Open Scope category_scope.
 Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }.
-Class Isomorphic {C : PreCategory} s d := { morphism_isomorphic :> @morphism C s d ; isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+Class Isomorphic {C : PreCategory} s d := { morphism_isomorphic :: @morphism C s d ; isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic }.
 Coercion morphism_isomorphic : Isomorphic >-> morphism.
 Local Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
 Definition idtoiso (C : PreCategory) (x y : C) (H : x = y) : Isomorphic x y := admit.

diff --git a/test-suite/bugs/bug_3513.v b/test-suite/bugs/bug_3513.v
@@ -10,7 +10,7 @@ Class ILogicOps Frm := { lentails: relation Frm;
                          land: Frm -> Frm -> Frm;
                          lor: Frm -> Frm -> Frm }.
 Infix "|--"  := lentails (at level 79, no associativity).
-Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
+Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre :: PreOrder lentails }.
 Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
 Infix "-|-"  := lequiv (at level 85, no associativity).
 #[export] Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.

diff --git a/test-suite/bugs/bug_3647.v b/test-suite/bugs/bug_3647.v
@@ -266,7 +266,7 @@ Notation "'Exists' x .. y , p" :=
   (lexists (fun x => .. (lexists (fun y => p)) .. )) (at level 78, x binder, y binder, right associativity).
 
 Class ILogic Frm {ILOps: ILogicOps Frm} := {
-                                            lentailsPre:> PreOrder lentails;
+                                            lentailsPre :: PreOrder lentails;
                                             ltrueR: forall C, C |-- ltrue;
                                             lfalseL: forall C, lfalse |-- C;
                                             lforallL: forall T x (P: T -> Frm) C, P x |-- C -> lforall P |-- C;

diff --git a/test-suite/bugs/bug_3661.v b/test-suite/bugs/bug_3661.v
@@ -15,8 +15,8 @@ Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_i
 Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
 Unset Primitive Projections.
 Class Isomorphic {C : PreCategory} s d :=
-  { morphism_isomorphic :> morphism C s d;
-    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+  { morphism_isomorphic :: morphism C s d;
+    isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic }.
 Arguments morphism_inverse {C s d} m {_} / .
 Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope.
 Definition functor_category (C D : PreCategory) : PreCategory.

diff --git a/test-suite/bugs/bug_3699.v b/test-suite/bugs/bug_3699.v
@@ -21,12 +21,12 @@ Module NonPrim.
   Notation "x .1" := (pr1 x) : fibration_scope.
   Notation "x .2" := (pr2 x) : fibration_scope.
   Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
-  Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
+  Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :: Contr (Trunc n A).
   Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
                                   (C : Type) `{IsTrunc n C} (f : A -> C),
                              { c:C & forall a:A, f a = c }.
   Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
-    := isconnected_hfiber_conn_map :> forall b:B, IsConnected n (hfiber f b).
+    := isconnected_hfiber_conn_map :: forall b:B, IsConnected n (hfiber f b).
   Definition conn_map_elim {n : trunc_index}
              {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
              (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
@@ -96,12 +96,12 @@ Module Prim.
   Notation "x .1" := (pr1 x) : fibration_scope.
   Notation "x .2" := (pr2 x) : fibration_scope.
   Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
-  Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
+  Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :: Contr (Trunc n A).
   Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
                                   (C : Type) `{IsTrunc n C} (f : A -> C),
                              { c:C & forall a:A, f a = c }.
   Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
-    := isconnected_hfiber_conn_map :> forall b:B, IsConnected n (hfiber f b).
+    := isconnected_hfiber_conn_map :: forall b:B, IsConnected n (hfiber f b).
   Definition conn_map_elim {n : trunc_index}
              {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
              (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}

diff --git a/test-suite/bugs/bug_3943.v b/test-suite/bugs/bug_3943.v
@@ -35,8 +35,8 @@ Arguments morphism_inverse {C s d} m {_}.
 Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope.
 
 Class Isomorphic {C : PreCategory} s d := {
-    morphism_isomorphic :> morphism C s d;
-    isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
+    morphism_isomorphic :: morphism C s d;
+    isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic }.
 Coercion morphism_isomorphic : Isomorphic >-> morphism.
 
 Variable C : PreCategory.

diff --git a/test-suite/bugs/bug_3960.v b/test-suite/bugs/bug_3960.v
@@ -16,7 +16,7 @@ Class myClass (A: Type) :=
 
 Class myClassP (A : Type)  :=
   {
-    super :> myClass A;
+    super :: myClass A;
     barP : forall (a : A), bar a
   }.
 

diff --git a/test-suite/bugs/bug_4095.v b/test-suite/bugs/bug_4095.v
@@ -12,7 +12,7 @@ Class ILogicOps Frm := { lentails: relation Frm;
                          land: Frm -> Frm -> Frm;
                          lor: Frm -> Frm -> Frm }.
 Infix "|--"  := lentails (at level 79, no associativity).
-Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
+Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre :: PreOrder lentails }.
 Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
 Infix "-|-"  := lequiv (at level 85, no associativity).
 #[export] Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.

diff --git a/test-suite/bugs/bug_4116.v b/test-suite/bugs/bug_4116.v
@@ -251,8 +251,8 @@ Module Export Morphisms.
 
   Class Isomorphic {C : PreCategory} s d :=
     {
-      morphism_isomorphic :> morphism C s d;
-      isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
+      morphism_isomorphic :: morphism C s d;
+      isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic
     }.
 
   Coercion morphism_isomorphic : Isomorphic >-> morphism.