Skip to content

Commit a091b25

Browse files
coqbot-app[bot]SkySkimmer
coqbot-app[bot]
and
SkySkimmer
authored
Merge PR #18590: Uniformize semantics of :> in class after deprecation phase of #16230
Reviewed-by: SkySkimmer Ack-by: JasonGross Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>
2 parents 4c3f2e2 + 55b5f53 commit a091b25

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

47 files changed

+141
-101
lines changed

‎doc/changelog/02-specification-language/18590-cleanup_16230.rst

+51
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
- **Changed:**
2+
warnings `future-coercion-class-constructor`
3+
and `future-coercion-class-field` about ``:>`` in :cmd:`Class` as
4+
error by default. This offers a last opportunity to replace ``:>``
5+
with ``::`` (available since Coq 8.18) to declare typeclass instances
6+
before making ``:>`` consistently declare coercions in all records in
7+
next version.
8+
To adapt huge codebases, you can try
9+
`this script <https://gist.github.com/JasonGross/59fc3c03664f2280849abf50b531be42>`_
10+
or the one below. But beware that both are incomplete.
11+
12+
.. code-block:: sh
13+
14+
#!/bin/awk -f
15+
BEGIN {
16+
startclass = 0;
17+
inclass = 0;
18+
indefclass = 0; # definitionalclasses (single field, without { ... })
19+
}
20+
{
21+
if ($0 ~ "[ ]*Class") {
22+
startclass = 1;
23+
}
24+
if (startclass == 1 && $0 ~ ":=") {
25+
inclass = 1;
26+
indefclass = 1;
27+
}
28+
if (startclass == 1 && $0 ~ ":=.*{") {
29+
indefclass = 0;
30+
}
31+
if (inclass == 1) startclass = 0;
32+
33+
if (inclass == 1 && $0 ~ ":>") {
34+
if ($0 ~ "{ .*:>") { # first field on a single line
35+
sub("{ ", "{ #[global] ");
36+
} else if ($0 ~ ":=.*:>") { # definitional classes on a single line
37+
sub(":= ", ":= #[global] ");
38+
} else if ($0 ~ "^ ") {
39+
sub(" ", " #[global] ");
40+
} else {
41+
$0 = "#[global] " $0;
42+
}
43+
sub(":>", "::")
44+
}
45+
print $0;
46+
47+
if ($0 ~ ".*}[.]" || indefclass == 1 && $0 ~ "[.]$") inclass = 0;
48+
}
49+
50+
(`#18590 <https://github.com/coq/coq/pull/18590>`_,
51+
by Pierre Roux).

‎doc/sphinx/addendum/type-classes.rst

+1-1
Original file line numberDiff line numberDiff line change
@@ -248,7 +248,7 @@ the implicit arguments mechanism if available, as shown in the example.
248248
Substructures
249249
~~~~~~~~~~~~~
250250

251-
.. index:: :> (substructure)
251+
.. index:: :: (substructure)
252252

253253
Substructures are components of a typeclass which are themselves instances of a
254254
typeclass. They often arise when using typeclasses for logical properties, e.g.:

‎test-suite/bugs/HoTT_coq_058.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ Local Open Scope equiv_scope.
3030

3131
Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
3232

33-
Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
33+
Class Funext := { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
3434

3535
Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
3636
(forall x, f x = g x) -> f = g

‎test-suite/bugs/HoTT_coq_059.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Inductive eq {A} (x : A) : A -> Type := eq_refl : eq x x.
55
Notation "a = b" := (eq a b) : type_scope.
66

77
Section foo.
8-
Class Funext := { path_forall :> forall A P (f g : forall x : A, P x), (forall x, f x = g x) -> f = g }.
8+
Class Funext := { path_forall :: forall A P (f g : forall x : A, P x), (forall x, f x = g x) -> f = g }.
99
Context `{Funext, Funext}.
1010

1111
Set Printing Universes.

‎test-suite/bugs/HoTT_coq_062.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ Definition equiv_path (A B : Type) (p : A = B) : A <~> B
5252
:= BuildEquiv _ _ (transport (fun X:Type => X) p) admit.
5353

5454
Class Univalence :=
55-
isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B) .
55+
isequiv_equiv_path :: forall (A B : Type), IsEquiv (equiv_path A B) .
5656

5757
Section Univalence.
5858
Context `{Univalence}.

‎test-suite/bugs/HoTT_coq_088.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ Definition equiv_path (A B : Type) (p : A = B) : Equiv A B.
3535
Admitted.
3636

3737
Class Univalence := {
38-
isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
38+
isequiv_equiv_path :: forall (A B : Type), IsEquiv (equiv_path A B)
3939
}.
4040

4141
Definition ua_downward_closed `{Univalence} : Univalence.

‎test-suite/bugs/HoTT_coq_108.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ Notation Contr := (IsTrunc minus_two).
6161
Notation IsHSet := (IsTrunc 0).
6262

6363
Class Funext :=
64-
{ isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
64+
{ isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
6565
Global Instance contr_forall `{Funext} `{P : A -> Type} `{forall a, Contr (P a)}
6666
: Contr (forall a, P a) | 100.
6767
admit.

‎test-suite/bugs/HoTT_coq_112.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ Definition equiv_path (A B : Type) (p : A = B) : A <~> B
4242
:= BuildEquiv _ _ (transport (fun X:Type => X) p) _.
4343

4444
Class Univalence := {
45-
isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
45+
isequiv_equiv_path :: forall (A B : Type), IsEquiv (equiv_path A B)
4646
}.
4747

4848
Section Univalence.

‎test-suite/bugs/HoTT_coq_123.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type :=
4646
Notation IsHSet := (IsTrunc minus_two).
4747

4848
Class Funext :=
49-
{ isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
49+
{ isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
5050

5151
Local Open Scope equiv_scope.
5252

‎test-suite/bugs/bug_14221.v

+3-3
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
1414

1515
Class Setoid A := {
1616
equiv : crelation A;
17-
setoid_equiv :> Equivalence equiv
17+
setoid_equiv :: Equivalence equiv
1818
}.
1919

2020
Notation "f ≈ g" := (equiv f g) (at level 79).
@@ -46,7 +46,7 @@ Class Category := {
4646

4747
uhom := Type : Type;
4848
hom : obj -> obj -> uhom where "a ~> b" := (hom a b);
49-
homset :> ∀ X Y, Setoid (X ~> Y);
49+
homset :: ∀ X Y, Setoid (X ~> Y);
5050

5151
id {x} : x ~> x;
5252
}.
@@ -71,7 +71,7 @@ Class Functor (C D : Category) := {
7171
fobj : C -> D;
7272
fmap {x y : C} (f : x ~> y) : fobj x ~> fobj y;
7373

74-
fmap_respects :> ∀ x y, Proper (equiv ==> equiv) (@fmap x y);
74+
fmap_respects :: ∀ x y, Proper (equiv ==> equiv) (@fmap x y);
7575

7676
fmap_id {x : C} : fmap (@id C x) ≈ id;
7777
}.

‎test-suite/bugs/bug_15099.v

+3-3
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ Set Universe Polymorphism.
88

99
Class Setoid A := {
1010
equiv : crelation A;
11-
setoid_equiv :> Equivalence equiv
11+
setoid_equiv :: Equivalence equiv
1212
}.
1313

1414
Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope.
@@ -19,7 +19,7 @@ Class Category := {
1919
obj : Type;
2020

2121
hom : obj -> obj -> Type where "a ~> b" := (hom a b);
22-
homset :> forall X Y, Setoid (X ~> Y);
22+
homset :: forall X Y, Setoid (X ~> Y);
2323

2424
id {x} : x ~> x;
2525

@@ -38,7 +38,7 @@ Class Functor {C D : Category} := {
3838
fobj : C -> D;
3939
fmap {x y : C} (f : x ~> y) : fobj x ~> fobj y;
4040

41-
fmap_respects :> forall x y, Proper (equiv ==> equiv) (@fmap x y);
41+
fmap_respects :: forall x y, Proper (equiv ==> equiv) (@fmap x y);
4242

4343
fmap_id {x : C} : fmap (@id C x) ≈ id;
4444
}.

‎test-suite/bugs/bug_16204.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Class IsProp (A : Type) : Prop :=
66
irrel (x y : A) : x = y.
77

88
Class IsProofIrrel : Prop :=
9-
proof_irrel (A : Prop) :> IsProp A.
9+
proof_irrel (A : Prop) :: IsProp A.
1010

1111
Class IsPropExt : Prop :=
1212
prop_ext (A B : Prop) (a : A <-> B) : A = B.

‎test-suite/bugs/bug_3321.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A ; e
77
Record Equiv A B := BuildEquiv { equiv_fun :> A -> B ; equiv_isequiv :> IsEquiv equiv_fun }.
88
Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
99
Definition equiv_path (A B : Type) (p : A = B) : Equiv A B := admit.
10-
Class Univalence := { isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B) }.
10+
Class Univalence := { isequiv_equiv_path :: forall (A B : Type), IsEquiv (equiv_path A B) }.
1111
Definition path_universe `{Univalence} {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B) := admit.
1212
Context `{ua:Univalence}.
1313
Variable A:Type.

‎test-suite/bugs/bug_3329.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
1515
:= fun x => match h with idpath => idpath end.
1616
Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
1717
Class IsHSet (A : Type) := { _ : False }.
18-
Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
18+
Class Funext := { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
1919
Record PreCategory :=
2020
{ object :> Type;
2121
morphism : object -> object -> Type;

‎test-suite/bugs/bug_3330.v

+3-3
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type :=
132132
Notation IsHSet := (IsTrunc 0).
133133

134134
Class Funext :=
135-
{ isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
135+
{ isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
136136

137137
Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
138138
f == g -> f = g
@@ -357,8 +357,8 @@ Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) :=
357357

358358
Class Isomorphic {C : PreCategory} s d :=
359359
{
360-
morphism_isomorphic :> morphism C s d;
361-
isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
360+
morphism_isomorphic :: morphism C s d;
361+
isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic
362362
}.
363363

364364
Module Export CategoryMorphismsNotations.

‎test-suite/bugs/bug_3393.v

+3-3
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
1313
Delimit Scope equiv_scope with equiv.
1414
Local Open Scope equiv_scope.
1515
Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
16-
Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
16+
Class Funext := { isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
1717
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.
1818
Record PreCategory :=
1919
{ object :> Type;
@@ -33,8 +33,8 @@ Notation "F '_1' m" := (@morphism_of _ _ F _ _ m) (at level 10, no associativity
3333
Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }.
3434
Local Notation "m ^-1" := (morphism_inverse (m := m)) : morphism_scope.
3535
Class Isomorphic {C : PreCategory} s d :=
36-
{ morphism_isomorphic :> morphism C s d;
37-
isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
36+
{ morphism_isomorphic :: morphism C s d;
37+
isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic }.
3838
Coercion morphism_isomorphic : Isomorphic >-> morphism.
3939
Definition isisomorphism_inverse `(@IsIsomorphism C x y m) : IsIsomorphism m^-1 := {| morphism_inverse := m |}.
4040

‎test-suite/bugs/bug_3422.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -52,8 +52,8 @@ Local Notation "m ^-1" := (morphism_inverse (m := m)) : morphism_scope.
5252

5353
Class Isomorphic {C : PreCategory} s d :=
5454
{
55-
morphism_isomorphic :> morphism C s d;
56-
isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
55+
morphism_isomorphic :: morphism C s d;
56+
isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic
5757
}.
5858

5959
Coercion morphism_isomorphic : Isomorphic >-> morphism.

‎test-suite/bugs/bug_3427.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ Notation IsHProp := (IsTrunc minus_one).
7474
Notation IsHSet := (IsTrunc 0).
7575

7676
Class Funext :=
77-
{ isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
77+
{ isequiv_apD10 :: forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
7878

7979
Definition concat_pV {A : Type} {x y : A} (p : x = y) :
8080
p @ p^ = 1
@@ -136,7 +136,7 @@ Definition equiv_path (A B : Type) (p : A = B) : A <~> B
136136
:= BuildEquiv _ _ (transport (fun X:Type => X) p) _.
137137

138138
Class Univalence := {
139-
isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B)
139+
isequiv_equiv_path :: forall (A B : Type), IsEquiv (equiv_path A B)
140140
}.
141141

142142
Section Univalence.

‎test-suite/bugs/bug_3480.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Delimit Scope category_scope with category.
1010
Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
1111
Local Open Scope category_scope.
1212
Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }.
13-
Class Isomorphic {C : PreCategory} s d := { morphism_isomorphic :> @morphism C s d ; isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
13+
Class Isomorphic {C : PreCategory} s d := { morphism_isomorphic :: @morphism C s d ; isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic }.
1414
Coercion morphism_isomorphic : Isomorphic >-> morphism.
1515
Local Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope.
1616
Definition idtoiso (C : PreCategory) (x y : C) (H : x = y) : Isomorphic x y := admit.

‎test-suite/bugs/bug_3513.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Class ILogicOps Frm := { lentails: relation Frm;
1010
land: Frm -> Frm -> Frm;
1111
lor: Frm -> Frm -> Frm }.
1212
Infix "|--" := lentails (at level 79, no associativity).
13-
Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
13+
Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre :: PreOrder lentails }.
1414
Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
1515
Infix "-|-" := lequiv (at level 85, no associativity).
1616
#[export] Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.

‎test-suite/bugs/bug_3647.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -266,7 +266,7 @@ Notation "'Exists' x .. y , p" :=
266266
(lexists (fun x => .. (lexists (fun y => p)) .. )) (at level 78, x binder, y binder, right associativity).
267267

268268
Class ILogic Frm {ILOps: ILogicOps Frm} := {
269-
lentailsPre:> PreOrder lentails;
269+
lentailsPre :: PreOrder lentails;
270270
ltrueR: forall C, C |-- ltrue;
271271
lfalseL: forall C, lfalse |-- C;
272272
lforallL: forall T x (P: T -> Frm) C, P x |-- C -> lforall P |-- C;

‎test-suite/bugs/bug_3661.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_i
1515
Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
1616
Unset Primitive Projections.
1717
Class Isomorphic {C : PreCategory} s d :=
18-
{ morphism_isomorphic :> morphism C s d;
19-
isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
18+
{ morphism_isomorphic :: morphism C s d;
19+
isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic }.
2020
Arguments morphism_inverse {C s d} m {_} / .
2121
Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope.
2222
Definition functor_category (C D : PreCategory) : PreCategory.

‎test-suite/bugs/bug_3699.v

+4-4
Original file line numberDiff line numberDiff line change
@@ -21,12 +21,12 @@ Module NonPrim.
2121
Notation "x .1" := (pr1 x) : fibration_scope.
2222
Notation "x .2" := (pr2 x) : fibration_scope.
2323
Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
24-
Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
24+
Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :: Contr (Trunc n A).
2525
Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
2626
(C : Type) `{IsTrunc n C} (f : A -> C),
2727
{ c:C & forall a:A, f a = c }.
2828
Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
29-
:= isconnected_hfiber_conn_map :> forall b:B, IsConnected n (hfiber f b).
29+
:= isconnected_hfiber_conn_map :: forall b:B, IsConnected n (hfiber f b).
3030
Definition conn_map_elim {n : trunc_index}
3131
{A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
3232
(P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
@@ -96,12 +96,12 @@ Module Prim.
9696
Notation "x .1" := (pr1 x) : fibration_scope.
9797
Notation "x .2" := (pr2 x) : fibration_scope.
9898
Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
99-
Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
99+
Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :: Contr (Trunc n A).
100100
Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
101101
(C : Type) `{IsTrunc n C} (f : A -> C),
102102
{ c:C & forall a:A, f a = c }.
103103
Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
104-
:= isconnected_hfiber_conn_map :> forall b:B, IsConnected n (hfiber f b).
104+
:= isconnected_hfiber_conn_map :: forall b:B, IsConnected n (hfiber f b).
105105
Definition conn_map_elim {n : trunc_index}
106106
{A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
107107
(P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}

‎test-suite/bugs/bug_3943.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -35,8 +35,8 @@ Arguments morphism_inverse {C s d} m {_}.
3535
Local Notation "m ^-1" := (morphism_inverse m) (at level 3, format "m '^-1'") : morphism_scope.
3636

3737
Class Isomorphic {C : PreCategory} s d := {
38-
morphism_isomorphic :> morphism C s d;
39-
isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }.
38+
morphism_isomorphic :: morphism C s d;
39+
isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic }.
4040
Coercion morphism_isomorphic : Isomorphic >-> morphism.
4141

4242
Variable C : PreCategory.

‎test-suite/bugs/bug_3960.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ Class myClass (A: Type) :=
1616

1717
Class myClassP (A : Type) :=
1818
{
19-
super :> myClass A;
19+
super :: myClass A;
2020
barP : forall (a : A), bar a
2121
}.
2222

‎test-suite/bugs/bug_4095.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Class ILogicOps Frm := { lentails: relation Frm;
1212
land: Frm -> Frm -> Frm;
1313
lor: Frm -> Frm -> Frm }.
1414
Infix "|--" := lentails (at level 79, no associativity).
15-
Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
15+
Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre :: PreOrder lentails }.
1616
Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
1717
Infix "-|-" := lequiv (at level 85, no associativity).
1818
#[export] Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.

‎test-suite/bugs/bug_4116.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -251,8 +251,8 @@ Module Export Morphisms.
251251

252252
Class Isomorphic {C : PreCategory} s d :=
253253
{
254-
morphism_isomorphic :> morphism C s d;
255-
isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic
254+
morphism_isomorphic :: morphism C s d;
255+
isisomorphism_isomorphic :: IsIsomorphism morphism_isomorphic
256256
}.
257257

258258
Coercion morphism_isomorphic : Isomorphic >-> morphism.

0 commit comments

Comments
 (0)