Skip to content

Commit dc26512

Browse files
proux01proux01
committed
[test-suite] Remove deprecated :> in Class
Replace them with the new :: syntax.
1 parent c3c67fa commit dc26512

32 files changed

+70
-81
lines changed

‎test-suite/bugs/HoTT_coq_058.v

Lines changed: 1 addition & 1 deletion
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_062.v

Lines changed: 1 addition & 1 deletion
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_112.v

Lines changed: 1 addition & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 1 addition & 1 deletion
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_3330.v

Lines changed: 3 additions & 3 deletions
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

Lines changed: 3 additions & 3 deletions
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

Lines changed: 2 additions & 2 deletions
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

Lines changed: 2 additions & 2 deletions
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 1 addition & 1 deletion
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

Lines changed: 2 additions & 2 deletions
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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ Module NonPrim.
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) (at level 3, format "x '.1'") : fibration_scope.
9797
Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : 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

Lines changed: 2 additions & 2 deletions
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_4095.v

Lines changed: 1 addition & 1 deletion
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

Lines changed: 2 additions & 2 deletions
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.

‎test-suite/bugs/bug_4151.v

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ Module Export BaseTypes.
148148
ntl_wf : well_founded nonterminals_listT_R }.
149149

150150
Class parser_computational_types_dataT :=
151-
{ predata :> parser_computational_predataT;
151+
{ predata :: parser_computational_predataT;
152152
split_stateT : String -> nonterminals_listT -> any_grammar CharType -> String -> Type }.
153153

154154
Class parser_computational_dataT' `{parser_computational_types_dataT} :=
@@ -242,9 +242,9 @@ Section general.
242242
Context {CharType} {String : string_like CharType} {G : grammar CharType}.
243243

244244
Class boolean_parser_dataT :=
245-
{ predata :> parser_computational_predataT;
245+
{ predata :: parser_computational_predataT;
246246
split_stateT : String -> Type;
247-
data' :> _ := {| BaseTypes.predata := predata ; BaseTypes.split_stateT := fun _ _ _ => split_stateT |};
247+
data' :: _ := {| BaseTypes.predata := predata ; BaseTypes.split_stateT := fun _ _ _ => split_stateT |};
248248
split_string_for_production
249249
: forall it its,
250250
StringWithSplitState String split_stateT
@@ -254,7 +254,7 @@ Section general.
254254
let P f := List.Forall f (split_string_for_production it its str) in
255255
P (fun s1s2 =>
256256
(fst s1s2 ++ snd s1s2 =s str) = true);
257-
premethods :> parser_computational_dataT'
257+
premethods :: parser_computational_dataT'
258258
:= @Build_parser_computational_dataT'
259259
_ String data'
260260
(fun _ _ => split_string_for_production)

‎test-suite/bugs/bug_4187.v

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ Import Coq.Classes.Morphisms.
131131
Module Export StringLike.
132132
Class StringLike {Char : Type} :=
133133
{
134-
String :> Type;
134+
String :: Type;
135135
is_char : String -> Char -> bool;
136136
length : String -> nat;
137137
take : nat -> String -> String;
@@ -154,11 +154,11 @@ Module Export StringLike.
154154
singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch';
155155
length_singleton : forall s ch, s ~= [ ch ] -> length s = 1;
156156
bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s';
157-
is_char_Proper :> Proper (beq ==> eq ==> eq) is_char;
158-
length_Proper :> Proper (beq ==> eq) length;
159-
take_Proper :> Proper (eq ==> beq ==> beq) take;
160-
drop_Proper :> Proper (eq ==> beq ==> beq) drop;
161-
bool_eq_Equivalence :> Equivalence beq;
157+
is_char_Proper :: Proper (beq ==> eq ==> eq) is_char;
158+
length_Proper :: Proper (beq ==> eq) length;
159+
take_Proper :: Proper (eq ==> beq ==> beq) take;
160+
drop_Proper :: Proper (eq ==> beq ==> beq) drop;
161+
bool_eq_Equivalence :: Equivalence beq;
162162
bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str';
163163
take_short_length : forall str n, n <= length str -> length (take n str) = n;
164164
take_long : forall str n, length str <= n -> take n str =s str;
@@ -340,7 +340,7 @@ Section general.
340340
Context {Char} {HSL : StringLike Char} {G : grammar Char}.
341341

342342
Class boolean_parser_dataT :=
343-
{ predata :> parser_computational_predataT;
343+
{ predata :: parser_computational_predataT;
344344
split_string_for_production
345345
: item Char -> production Char -> String -> list nat }.
346346

‎test-suite/bugs/bug_4232.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
Require Import Setoid Morphisms Vector.
22

33
Class Equiv A := equiv : A -> A -> Prop.
4-
Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).
4+
Class Setoid A `{Equiv A} := setoid_equiv :: Equivalence (equiv).
55

66
Global Declare Instance vec_equiv {A} `{Equiv A} {n}: Equiv (Vector.t A n).
77
Global Declare Instance vec_setoid A `{Setoid A} n : Setoid (Vector.t A n).

‎test-suite/bugs/bug_4456.v

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ Local Coercion is_true : bool >-> Sortclass.
5151
Module Export StringLike.
5252
Class StringLike {Char : Type} :=
5353
{
54-
String :> Type;
54+
String :: Type;
5555
is_char : String -> Char -> bool;
5656
length : String -> nat;
5757
take : nat -> String -> String;
@@ -76,11 +76,11 @@ Module Export StringLike.
7676
unsafe_get_correct : forall n s ch, get n s = Some ch -> unsafe_get n s = ch;
7777
length_singleton : forall s ch, s ~= [ ch ] -> length s = 1;
7878
bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s';
79-
is_char_Proper :> Proper (beq ==> eq ==> eq) is_char;
80-
length_Proper :> Proper (beq ==> eq) length;
81-
take_Proper :> Proper (eq ==> beq ==> beq) take;
82-
drop_Proper :> Proper (eq ==> beq ==> beq) drop;
83-
bool_eq_Equivalence :> Equivalence beq;
79+
is_char_Proper :: Proper (beq ==> eq ==> eq) is_char;
80+
length_Proper :: Proper (beq ==> eq) length;
81+
take_Proper :: Proper (eq ==> beq ==> beq) take;
82+
drop_Proper :: Proper (eq ==> beq ==> beq) drop;
83+
bool_eq_Equivalence :: Equivalence beq;
8484
bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str';
8585
take_short_length : forall str n, n <= length str -> length (take n str) = n;
8686
take_long : forall str n, length str <= n -> take n str =s str;
@@ -211,8 +211,8 @@ Section recursive_descent_parser.
211211
: item Char -> production Char -> String -> list nat }.
212212

213213
Class boolean_parser_dataT :=
214-
{ predata :> parser_computational_predataT;
215-
split_data :> split_dataT }.
214+
{ predata :: parser_computational_predataT;
215+
split_data :: split_dataT }.
216216
End recursive_descent_parser.
217217

218218
End BaseTypes.

‎test-suite/bugs/bug_7916.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -166,7 +166,7 @@ Module Iris.
166166
Global Arguments decide _ {_} : simpl never, assert.
167167

168168
Class RelDecision {A B} (R : A → B → Prop) :=
169-
decide_rel x y :> Decision (R x y).
169+
decide_rel x y :: Decision (R x y).
170170
Notation EqDecision A := (RelDecision (=@{A})).
171171

172172
Class Inj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop :=

‎test-suite/bugs/bug_8004.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ Infix "∧" := prod (at level 80, right associativity) : category_theory_scope.
99

1010
Class Setoid A := {
1111
equiv : crelation A;
12-
setoid_equiv :> Equivalence equiv
12+
setoid_equiv :: Equivalence equiv
1313
}.
1414

1515
Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope.

0 commit comments

Comments
 (0)