Skip to content

Fix deprecation warnings #157

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Fix deprecation warnings #157

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Adjunction/Hom.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -279,4 +279,4 @@ Qed.

End AdjunctionHom.

Arguments Adjunction_Hom {C D} F%functor U%functor.
Arguments Adjunction_Hom {C D} F%_functor U%_functor.
2 changes: 1 addition & 1 deletion Adjunction/Natural/Transformation.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ Class Adjunction_Transform := {

End AdjunctionTransform.

Arguments Adjunction_Transform {C D} F%functor U%functor.
Arguments Adjunction_Transform {C D} F%_functor U%_functor.

Declare Scope adjunction_scope.
Declare Scope adjunction_type_scope.
Expand Down
4 changes: 2 additions & 2 deletions Structure/End.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,8 @@ Class End `(F : C^op ∏ C ⟶ D) := {
wedge_map[end_wedge] ∘ u ≈ @wedge_map _ _ _ W x
}.

Arguments End {_%category _%category} F%functor.
Arguments end_wedge {_%category _%category} F%functor {_}.
Arguments End {_%_category _%_category} F%_functor.
Arguments end_wedge {_%_category _%_category} F%_functor {_}.

Coercion wedge_obj `(F : C^op ∏ C ⟶ D) (E : End F) := @end_wedge _ _ _ E.

Expand Down
4 changes: 2 additions & 2 deletions Structure/Pullback/Limit.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,10 +12,10 @@ Require Import Category.Instance.Roof.
Generalizable All Variables.

Definition Pullback_Limit {C : Category} (F : Cospan C) := Limit F.
Arguments Pullback_Limit {_%category} F%functor /.
Arguments Pullback_Limit {_%_category} F%_functor /.

Definition Pushout_Limit {C : Category} (F : Span C) := Colimit F.
Arguments Pushout_Limit {_%category} F%functor /.
Arguments Pushout_Limit {_%_category} F%_functor /.

Program Definition Pullback_to_Universal {C : Category}
(F : Cospan C) (P : Pullback_Limit F) :
Expand Down
2 changes: 1 addition & 1 deletion Theory/Adjunction.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -248,7 +248,7 @@ Proof. intros; now rewrites. Qed.

End Adjunction.

Arguments Adjunction {C D} F%functor U%functor.
Arguments Adjunction {C D} F%_functor U%_functor.

Declare Scope adjunction_scope.
Declare Scope adjunction_type_scope.
Expand Down
16 changes: 8 additions & 8 deletions Theory/Category.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,8 +67,8 @@
Delimit Scope homset_scope with homset.
Delimit Scope morphism_scope with morphism.

Arguments dom {_%category _%object _%object} _%morphism.
Arguments cod {_%category _%object _%object} _%morphism.
Arguments dom {_%_category _%_object _%_object} _%_morphism.

Check failure on line 70 in Theory/Category.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.14) 

Unknown scope delimiting key _category.

Check failure on line 70 in Theory/Category.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.18) 

Unknown scope delimiting key _category.

Check failure on line 70 in Theory/Category.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.17) 

Unknown scope delimiting key _category.

Check failure on line 70 in Theory/Category.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.15) 

Unknown scope delimiting key _category.

Check failure on line 70 in Theory/Category.v

View workflow job for this annotation

GitHub Actions / build (coqorg/coq:8.16) 

Unknown scope delimiting key _category.
Arguments cod {_%_category _%_object _%_object} _%_morphism.

Notation "obj[ C ]" := (@obj C%category)
(at level 0, format "obj[ C ]") : type_scope.
Expand Down Expand Up @@ -178,12 +178,12 @@

End Category.

Arguments dom {_%category _%object _%object} _%morphism.
Arguments cod {_%category _%object _%object} _%morphism.
Arguments id_left {_%category _%object _%object} _%morphism.
Arguments id_right {_%category _%object _%object} _%morphism.
Arguments comp_assoc {_%category _%object _%object _%object _%object}
_%morphism _%morphism _%morphism.
Arguments dom {_%_category _%_object _%_object} _%_morphism.
Arguments cod {_%_category _%_object _%_object} _%_morphism.
Arguments id_left {_%_category _%_object _%_object} _%_morphism.
Arguments id_right {_%_category _%_object _%_object} _%_morphism.
Arguments comp_assoc {_%_category _%_object _%_object _%_object _%_object}
_%_morphism _%_morphism _%_morphism.

#[export]
Program Instance hom_preorder {C : Category} : PreOrder (@hom C) := {
Expand Down
2 changes: 1 addition & 1 deletion Theory/Functor.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ Notation "C ⟶ D" := (@Functor C%category D%category)
(at level 90, right associativity) : functor_type_scope.

Arguments fmap
{C%category D%category Functor%functor x%object y%object} f%morphism.
{C%_category D%_category Functor%_functor x%_object y%_object} f%_morphism.

Infix "<$>" := fmap
(at level 29, left associativity, only parsing) : morphism_scope.
Expand Down
4 changes: 2 additions & 2 deletions Theory/Isomorphism.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -144,8 +144,8 @@ Notation "x ≅ y" := (@Isomorphism _%category x%object y%object)
Notation "x ≅[ C ] y" := (@Isomorphism C%category x%object y%object)
(at level 91, only parsing) : isomorphism_scope.

Arguments to {_%category x%object y%object} _%morphism.
Arguments from {_%category x%object y%object} _%morphism.
Arguments to {_%_category x%_object y%_object} _%_morphism.
Arguments from {_%_category x%_object y%_object} _%_morphism.
Arguments iso_to_from {_ _ _} _.
Arguments iso_from_to {_ _ _} _.

Expand Down