From 0f1cab7a1506ca55318023a8de256fb694f2e8e1 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 24 Apr 2026 12:28:53 +0000 Subject: [PATCH 1/2] Fix style issues from #2353: split two commands onto separate lines Agent-Logs-Url: https://github.com/HoTT/Coq-HoTT/sessions/60bd284b-46b1-4a39-a188-6f84406801fe Co-authored-by: Alizter <8614547+Alizter@users.noreply.github.com> --- theories/Basics/Settings.v | 3 ++- theories/Categories/Adjoint/Composition/AssociativityLaw.v | 3 ++- theories/Categories/Adjoint/Composition/Core.v | 3 ++- theories/Categories/Adjoint/Composition/IdentityLaws.v | 3 ++- theories/Categories/Adjoint/Composition/LawsTactic.v | 3 ++- theories/Categories/Adjoint/Dual.v | 3 ++- theories/Categories/Adjoint/Functorial/Core.v | 3 ++- theories/Categories/Adjoint/Functorial/Laws.v | 3 ++- theories/Categories/Adjoint/Functorial/Parts.v | 3 ++- theories/Categories/Adjoint/Hom.v | 3 ++- theories/Categories/Adjoint/HomCoercions.v | 3 ++- theories/Categories/Adjoint/Identity.v | 3 ++- theories/Categories/Adjoint/Paths.v | 3 ++- theories/Categories/Adjoint/Pointwise.v | 3 ++- theories/Categories/Adjoint/UnitCounit.v | 3 ++- theories/Categories/Adjoint/UnitCounitCoercions.v | 3 ++- theories/Categories/Adjoint/UniversalMorphisms/Core.v | 3 ++- theories/Categories/Cat/Core.v | 3 ++- theories/Categories/Cat/Morphisms.v | 3 ++- theories/Categories/Category/Core.v | 3 ++- theories/Categories/Category/Dual.v | 3 ++- theories/Categories/Category/Morphisms.v | 3 ++- theories/Categories/Category/Objects.v | 3 ++- theories/Categories/Category/Paths.v | 3 ++- theories/Categories/Category/Pi.v | 3 ++- theories/Categories/Category/Prod.v | 3 ++- theories/Categories/Category/Sigma/Core.v | 3 ++- theories/Categories/Category/Sigma/OnMorphisms.v | 3 ++- theories/Categories/Category/Sigma/OnObjects.v | 3 ++- theories/Categories/Category/Sigma/Univalent.v | 3 ++- theories/Categories/Category/Strict.v | 3 ++- theories/Categories/Category/Sum.v | 3 ++- theories/Categories/Category/Univalent.v | 3 ++- theories/Categories/CategoryOfGroupoids.v | 3 ++- theories/Categories/CategoryOfSections/Core.v | 3 ++- theories/Categories/ChainCategory.v | 3 ++- theories/Categories/Comma/Core.v | 3 ++- theories/Categories/Comma/Dual.v | 3 ++- theories/Categories/Comma/Functorial.v | 3 ++- theories/Categories/Comma/InducedFunctors.v | 3 ++- theories/Categories/Comma/Projection.v | 3 ++- theories/Categories/Comma/ProjectionFunctors.v | 3 ++- theories/Categories/DependentProduct.v | 3 ++- theories/Categories/DiscreteCategory.v | 3 ++- theories/Categories/DualFunctor.v | 3 ++- theories/Categories/ExponentialLaws/Law0.v | 3 ++- theories/Categories/ExponentialLaws/Law1/Functors.v | 3 ++- theories/Categories/ExponentialLaws/Law1/Law.v | 3 ++- theories/Categories/ExponentialLaws/Law2/Functors.v | 3 ++- theories/Categories/ExponentialLaws/Law2/Law.v | 3 ++- theories/Categories/ExponentialLaws/Law3/Functors.v | 3 ++- theories/Categories/ExponentialLaws/Law3/Law.v | 3 ++- theories/Categories/ExponentialLaws/Law4/Functors.v | 3 ++- theories/Categories/ExponentialLaws/Law4/Law.v | 3 ++- theories/Categories/Functor/Attributes.v | 3 ++- theories/Categories/Functor/Composition/Core.v | 3 ++- .../Categories/Functor/Composition/Functorial/Attributes.v | 3 ++- theories/Categories/Functor/Composition/Functorial/Core.v | 3 ++- theories/Categories/Functor/Composition/Laws.v | 3 ++- theories/Categories/Functor/Core.v | 3 ++- theories/Categories/Functor/Dual.v | 3 ++- theories/Categories/Functor/Identity.v | 3 ++- theories/Categories/Functor/Paths.v | 3 ++- theories/Categories/Functor/Pointwise/Core.v | 3 ++- theories/Categories/Functor/Pointwise/Properties.v | 3 ++- theories/Categories/Functor/Prod/Core.v | 3 ++- theories/Categories/Functor/Prod/Functorial.v | 3 ++- theories/Categories/Functor/Prod/Universal.v | 3 ++- theories/Categories/Functor/Sum.v | 3 ++- theories/Categories/FunctorCategory/Core.v | 3 ++- theories/Categories/FunctorCategory/Dual.v | 3 ++- theories/Categories/FunctorCategory/Functorial.v | 3 ++- theories/Categories/FunctorCategory/Morphisms.v | 3 ++- theories/Categories/FundamentalPreGroupoidCategory.v | 3 ++- theories/Categories/Grothendieck/PseudofunctorToCat.v | 3 ++- theories/Categories/Grothendieck/ToCat.v | 3 ++- theories/Categories/Grothendieck/ToSet/Core.v | 3 ++- theories/Categories/Grothendieck/ToSet/Morphisms.v | 3 ++- theories/Categories/Grothendieck/ToSet/Univalent.v | 3 ++- theories/Categories/GroupoidCategory/Core.v | 3 ++- theories/Categories/GroupoidCategory/Dual.v | 3 ++- theories/Categories/GroupoidCategory/Morphisms.v | 3 ++- theories/Categories/HomFunctor.v | 3 ++- theories/Categories/HomotopyPreCategory.v | 3 ++- theories/Categories/IndiscreteCategory.v | 3 ++- theories/Categories/InitialTerminalCategory/Core.v | 3 ++- theories/Categories/InitialTerminalCategory/Functors.v | 3 ++- .../InitialTerminalCategory/NaturalTransformations.v | 3 ++- theories/Categories/InitialTerminalCategory/Pseudofunctors.v | 3 ++- theories/Categories/KanExtensions/Core.v | 3 ++- theories/Categories/KanExtensions/Functors.v | 3 ++- theories/Categories/LaxComma/Core.v | 3 ++- theories/Categories/LaxComma/CoreLaws.v | 3 ++- theories/Categories/LaxComma/CoreParts.v | 3 ++- theories/Categories/Limits/Core.v | 3 ++- theories/Categories/Limits/Functors.v | 3 ++- theories/Categories/Monoidal/MonoidalCategory.v | 3 ++- theories/Categories/NatCategory.v | 3 ++- theories/Categories/NaturalTransformation/Composition/Core.v | 3 ++- .../Categories/NaturalTransformation/Composition/Functorial.v | 3 ++- theories/Categories/NaturalTransformation/Composition/Laws.v | 3 ++- theories/Categories/NaturalTransformation/Core.v | 3 ++- theories/Categories/NaturalTransformation/Dual.v | 3 ++- theories/Categories/NaturalTransformation/Identity.v | 3 ++- theories/Categories/NaturalTransformation/Isomorphisms.v | 3 ++- theories/Categories/NaturalTransformation/Paths.v | 3 ++- theories/Categories/NaturalTransformation/Pointwise.v | 3 ++- theories/Categories/NaturalTransformation/Prod.v | 3 ++- theories/Categories/NaturalTransformation/Sum.v | 3 ++- theories/Categories/ProductLaws.v | 3 ++- theories/Categories/Profunctor/Core.v | 3 ++- theories/Categories/Profunctor/Identity.v | 3 ++- theories/Categories/Profunctor/Representable.v | 3 ++- theories/Categories/Pseudofunctor/Core.v | 3 ++- theories/Categories/Pseudofunctor/FromFunctor.v | 3 ++- theories/Categories/Pseudofunctor/Identity.v | 3 ++- theories/Categories/Pseudofunctor/RewriteLaws.v | 3 ++- theories/Categories/PseudonaturalTransformation/Core.v | 3 ++- theories/Categories/SemiSimplicialSets.v | 3 ++- theories/Categories/SetCategory/Core.v | 3 ++- theories/Categories/SetCategory/Functors/SetProp.v | 3 ++- theories/Categories/SetCategory/Morphisms.v | 3 ++- theories/Categories/SimplicialSets.v | 3 ++- theories/Categories/Structure/Core.v | 3 ++- theories/Categories/Structure/IdentityPrinciple.v | 3 ++- theories/Categories/UniversalProperties.v | 3 ++- theories/Categories/Yoneda.v | 3 ++- 127 files changed, 254 insertions(+), 127 deletions(-) diff --git a/theories/Basics/Settings.v b/theories/Basics/Settings.v index 46d7594ebd9..e33cf0ea40d 100644 --- a/theories/Basics/Settings.v +++ b/theories/Basics/Settings.v @@ -42,7 +42,8 @@ Global Set Printing Primitive Projection Parameters. (** ** Pattern Matching *) (** This flag removes parameters from constructors in patterns that appear in a match statement. *) -Global Set Asymmetric Patterns. #[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits. +Global Set Asymmetric Patterns. +#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits. (** ** Unification *) diff --git a/theories/Categories/Adjoint/Composition/AssociativityLaw.v b/theories/Categories/Adjoint/Composition/AssociativityLaw.v index ffaa80735c4..bd4e1327026 100644 --- a/theories/Categories/Adjoint/Composition/AssociativityLaw.v +++ b/theories/Categories/Adjoint/Composition/AssociativityLaw.v @@ -7,7 +7,8 @@ Require Import Types.Sigma Types.Prod. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope adjunction_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Composition/Core.v b/theories/Categories/Adjoint/Composition/Core.v index 294cfacb513..5d5dc8e017c 100644 --- a/theories/Categories/Adjoint/Composition/Core.v +++ b/theories/Categories/Adjoint/Composition/Core.v @@ -10,7 +10,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/Adjoint/Composition/IdentityLaws.v b/theories/Categories/Adjoint/Composition/IdentityLaws.v index e7fb2f7510a..4bf5ab2b439 100644 --- a/theories/Categories/Adjoint/Composition/IdentityLaws.v +++ b/theories/Categories/Adjoint/Composition/IdentityLaws.v @@ -7,7 +7,8 @@ Require Import Types.Sigma Types.Prod. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope adjunction_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Composition/LawsTactic.v b/theories/Categories/Adjoint/Composition/LawsTactic.v index 5d224b12687..1ebce444122 100644 --- a/theories/Categories/Adjoint/Composition/LawsTactic.v +++ b/theories/Categories/Adjoint/Composition/LawsTactic.v @@ -7,7 +7,8 @@ Require Import PathGroupoids HoTT.Tactics Types.Prod Types.Forall. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Ltac law_t := rewrite !transport_path_prod'; simpl; diff --git a/theories/Categories/Adjoint/Dual.v b/theories/Categories/Adjoint/Dual.v index 3b992de31ae..4d132c6bab6 100644 --- a/theories/Categories/Adjoint/Dual.v +++ b/theories/Categories/Adjoint/Dual.v @@ -6,7 +6,8 @@ Require Import Adjoint.UnitCounit Adjoint.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/Adjoint/Functorial/Core.v b/theories/Categories/Adjoint/Functorial/Core.v index 6cf90862ca8..2429c5f3ccb 100644 --- a/theories/Categories/Adjoint/Functorial/Core.v +++ b/theories/Categories/Adjoint/Functorial/Core.v @@ -10,7 +10,8 @@ Require Import HoTT.Types.Prod. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Functorial/Laws.v b/theories/Categories/Adjoint/Functorial/Laws.v index dd841d46bbe..f2ed5ceeb31 100644 --- a/theories/Categories/Adjoint/Functorial/Laws.v +++ b/theories/Categories/Adjoint/Functorial/Laws.v @@ -13,7 +13,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Functorial/Parts.v b/theories/Categories/Adjoint/Functorial/Parts.v index badd5f8087a..4982922b1ba 100644 --- a/theories/Categories/Adjoint/Functorial/Parts.v +++ b/theories/Categories/Adjoint/Functorial/Parts.v @@ -8,7 +8,8 @@ Require Import Adjoint.Core Adjoint.UnitCounit Adjoint.Dual. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Hom.v b/theories/Categories/Adjoint/Hom.v index 940460aeee0..33e4ac11b0c 100644 --- a/theories/Categories/Adjoint/Hom.v +++ b/theories/Categories/Adjoint/Hom.v @@ -11,7 +11,8 @@ Require Import Functor.Identity. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/HomCoercions.v b/theories/Categories/Adjoint/HomCoercions.v index 5a07618a314..b67958bc3f6 100644 --- a/theories/Categories/Adjoint/HomCoercions.v +++ b/theories/Categories/Adjoint/HomCoercions.v @@ -11,7 +11,8 @@ Require Import Basics.Trunc Types.Sigma HoTT.Tactics Equivalences. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Identity.v b/theories/Categories/Adjoint/Identity.v index 37c4ec81133..dd45cde8130 100644 --- a/theories/Categories/Adjoint/Identity.v +++ b/theories/Categories/Adjoint/Identity.v @@ -6,7 +6,8 @@ Require Import Adjoint.UnitCounit Adjoint.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Section identity. (** There is an identity adjunction. It does the obvious thing. *) diff --git a/theories/Categories/Adjoint/Paths.v b/theories/Categories/Adjoint/Paths.v index 2a7f6893dc1..959ba80b307 100644 --- a/theories/Categories/Adjoint/Paths.v +++ b/theories/Categories/Adjoint/Paths.v @@ -8,7 +8,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/Adjoint/Pointwise.v b/theories/Categories/Adjoint/Pointwise.v index bee9d590c54..0837ee6fa4c 100644 --- a/theories/Categories/Adjoint/Pointwise.v +++ b/theories/Categories/Adjoint/Pointwise.v @@ -15,7 +15,8 @@ Require Import Basics.PathGroupoids HoTT.Tactics Types.Arrow. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope functor_scope. diff --git a/theories/Categories/Adjoint/UnitCounit.v b/theories/Categories/Adjoint/UnitCounit.v index d1677a2f119..ecc31bd9696 100644 --- a/theories/Categories/Adjoint/UnitCounit.v +++ b/theories/Categories/Adjoint/UnitCounit.v @@ -6,7 +6,8 @@ Require Import Functor.Composition.Core Functor.Identity. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/UnitCounitCoercions.v b/theories/Categories/Adjoint/UnitCounitCoercions.v index 08711be2cd5..7a83ba42d93 100644 --- a/theories/Categories/Adjoint/UnitCounitCoercions.v +++ b/theories/Categories/Adjoint/UnitCounitCoercions.v @@ -8,7 +8,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope category_scope. diff --git a/theories/Categories/Adjoint/UniversalMorphisms/Core.v b/theories/Categories/Adjoint/UniversalMorphisms/Core.v index e4ef3b2c712..4c023fc1dd9 100644 --- a/theories/Categories/Adjoint/UniversalMorphisms/Core.v +++ b/theories/Categories/Adjoint/UniversalMorphisms/Core.v @@ -12,7 +12,8 @@ Require Import UniversalProperties Comma.Dual InitialTerminalCategory.Core Initi Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Cat/Core.v b/theories/Categories/Cat/Core.v index a3ad64f3aa6..d9247f85fc3 100644 --- a/theories/Categories/Cat/Core.v +++ b/theories/Categories/Cat/Core.v @@ -5,7 +5,8 @@ Require Import Functor.Identity Functor.Composition.Core Functor.Composition.Law Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/Cat/Morphisms.v b/theories/Categories/Cat/Morphisms.v index 7765a03a372..3db08a14def 100644 --- a/theories/Categories/Cat/Morphisms.v +++ b/theories/Categories/Cat/Morphisms.v @@ -5,7 +5,8 @@ Require Import Category.Morphisms. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Core.v b/theories/Categories/Category/Core.v index 3e8ce50db3e..150213f8078 100644 --- a/theories/Categories/Category/Core.v +++ b/theories/Categories/Category/Core.v @@ -4,7 +4,8 @@ Require Export Overture Basics.Notations. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Declare Scope morphism_scope. Declare Scope category_scope. diff --git a/theories/Categories/Category/Dual.v b/theories/Categories/Category/Dual.v index 5e3192c5881..b27d5c9ac82 100644 --- a/theories/Categories/Category/Dual.v +++ b/theories/Categories/Category/Dual.v @@ -4,7 +4,8 @@ Require Import Category.Core Category.Objects. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Morphisms.v b/theories/Categories/Category/Morphisms.v index 3251a95c15a..0df9de8058c 100644 --- a/theories/Categories/Category/Morphisms.v +++ b/theories/Categories/Category/Morphisms.v @@ -5,7 +5,8 @@ Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Basics.Equivalences Type Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Objects.v b/theories/Categories/Category/Objects.v index 2ef90cd7879..36af18ea6e2 100644 --- a/theories/Categories/Category/Objects.v +++ b/theories/Categories/Category/Objects.v @@ -5,7 +5,8 @@ Require Import Category.Core Category.Morphisms. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Paths.v b/theories/Categories/Category/Paths.v index a67240c07eb..ecad6e25d11 100644 --- a/theories/Categories/Category/Paths.v +++ b/theories/Categories/Category/Paths.v @@ -7,7 +7,8 @@ Require Import HoTT.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope category_scope. diff --git a/theories/Categories/Category/Pi.v b/theories/Categories/Category/Pi.v index 865f58dabb3..d384cd20a96 100644 --- a/theories/Categories/Category/Pi.v +++ b/theories/Categories/Category/Pi.v @@ -5,7 +5,8 @@ Require Import Basics.Trunc. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Prod.v b/theories/Categories/Category/Prod.v index 683a89d9590..3aa5f104ec0 100644 --- a/theories/Categories/Category/Prod.v +++ b/theories/Categories/Category/Prod.v @@ -6,7 +6,8 @@ Require Import Types.Prod. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Sigma/Core.v b/theories/Categories/Category/Sigma/Core.v index ca68f449afe..d4e59db8353 100644 --- a/theories/Categories/Category/Sigma/Core.v +++ b/theories/Categories/Category/Sigma/Core.v @@ -5,7 +5,8 @@ Require Import Basics.Trunc Types.Sigma. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Notation sig_type := sig. diff --git a/theories/Categories/Category/Sigma/OnMorphisms.v b/theories/Categories/Category/Sigma/OnMorphisms.v index c68204e3786..130c7408622 100644 --- a/theories/Categories/Category/Sigma/OnMorphisms.v +++ b/theories/Categories/Category/Sigma/OnMorphisms.v @@ -9,7 +9,8 @@ Import Functor.Composition.Core.FunctorCompositionCoreNotations. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Notation sig_type := Overture.sig. Local Notation pr1_type := Overture.pr1. diff --git a/theories/Categories/Category/Sigma/OnObjects.v b/theories/Categories/Category/Sigma/OnObjects.v index 88887409a60..29d8833857d 100644 --- a/theories/Categories/Category/Sigma/OnObjects.v +++ b/theories/Categories/Category/Sigma/OnObjects.v @@ -9,7 +9,8 @@ Import Functor.Composition.Core.FunctorCompositionCoreNotations. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Notation sig_type := Overture.sig. Local Notation pr1_type := Overture.pr1. diff --git a/theories/Categories/Category/Sigma/Univalent.v b/theories/Categories/Category/Sigma/Univalent.v index 27d472176fb..3e441951e49 100644 --- a/theories/Categories/Category/Sigma/Univalent.v +++ b/theories/Categories/Category/Sigma/Univalent.v @@ -7,7 +7,8 @@ Require Import HoTT.Types HoTT.Basics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Notation pr1_type := Overture.pr1 (only parsing). diff --git a/theories/Categories/Category/Strict.v b/theories/Categories/Category/Strict.v index 5df37fe405f..8244bb821ea 100644 --- a/theories/Categories/Category/Strict.v +++ b/theories/Categories/Category/Strict.v @@ -4,7 +4,8 @@ Require Export Category.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Sum.v b/theories/Categories/Category/Sum.v index f5e01b8b2b9..c5c43566825 100644 --- a/theories/Categories/Category/Sum.v +++ b/theories/Categories/Category/Sum.v @@ -4,7 +4,8 @@ Require Export Category.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (** ** Definition of [+] for categories *) Section internals. diff --git a/theories/Categories/Category/Univalent.v b/theories/Categories/Category/Univalent.v index c1bd4c88b81..76fa6275fc0 100644 --- a/theories/Categories/Category/Univalent.v +++ b/theories/Categories/Category/Univalent.v @@ -5,7 +5,8 @@ Require Import HoTT.Basics HoTT.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/CategoryOfGroupoids.v b/theories/Categories/CategoryOfGroupoids.v index f019a1eb14e..f58fcc3305b 100644 --- a/theories/Categories/CategoryOfGroupoids.v +++ b/theories/Categories/CategoryOfGroupoids.v @@ -7,7 +7,8 @@ Require Import Functor.Paths. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/CategoryOfSections/Core.v b/theories/Categories/CategoryOfSections/Core.v index 98bf9cea100..538432ccd5c 100644 --- a/theories/Categories/CategoryOfSections/Core.v +++ b/theories/Categories/CategoryOfSections/Core.v @@ -9,7 +9,8 @@ Require Import HoTT.Basics HoTT.Types. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ChainCategory.v b/theories/Categories/ChainCategory.v index 85af68c94c6..70c9a7a0788 100644 --- a/theories/Categories/ChainCategory.v +++ b/theories/Categories/ChainCategory.v @@ -7,7 +7,8 @@ Require Import HoTT.Basics HoTT.Types HoTT.Spaces.Nat.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope nat_scope. diff --git a/theories/Categories/Comma/Core.v b/theories/Categories/Comma/Core.v index 48d37629c8a..c949bb55693 100644 --- a/theories/Categories/Comma/Core.v +++ b/theories/Categories/Comma/Core.v @@ -9,7 +9,8 @@ Import Functor.Identity.FunctorIdentityNotations. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Comma/Dual.v b/theories/Categories/Comma/Dual.v index e3b4a05e9d7..a76b4d37e75 100644 --- a/theories/Categories/Comma/Dual.v +++ b/theories/Categories/Comma/Dual.v @@ -10,7 +10,8 @@ Local Set Warnings "notation-overridden". Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Comma/Functorial.v b/theories/Categories/Comma/Functorial.v index 4463fcf748f..5bb00a58e1e 100644 --- a/theories/Categories/Comma/Functorial.v +++ b/theories/Categories/Comma/Functorial.v @@ -14,7 +14,8 @@ Require Import HoTT.Tactics PathGroupoids Types.Forall. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Comma/InducedFunctors.v b/theories/Categories/Comma/InducedFunctors.v index bf0fab941b6..42e45ccad81 100644 --- a/theories/Categories/Comma/InducedFunctors.v +++ b/theories/Categories/Comma/InducedFunctors.v @@ -15,7 +15,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. Local Open Scope category_scope. diff --git a/theories/Categories/Comma/Projection.v b/theories/Categories/Comma/Projection.v index 0a682aa381a..d7b64470b0f 100644 --- a/theories/Categories/Comma/Projection.v +++ b/theories/Categories/Comma/Projection.v @@ -12,7 +12,8 @@ Local Set Warnings "notation-overridden". (* work around bug #5567, https://coq. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. Local Open Scope category_scope. diff --git a/theories/Categories/Comma/ProjectionFunctors.v b/theories/Categories/Comma/ProjectionFunctors.v index 6702d7f67ab..f239ff64d54 100644 --- a/theories/Categories/Comma/ProjectionFunctors.v +++ b/theories/Categories/Comma/ProjectionFunctors.v @@ -18,7 +18,8 @@ Require Import Types.Forall PathGroupoids HoTT.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/DependentProduct.v b/theories/Categories/DependentProduct.v index 438aad41dd5..d59e36b5310 100644 --- a/theories/Categories/DependentProduct.v +++ b/theories/Categories/DependentProduct.v @@ -7,7 +7,8 @@ Require Import CategoryOfSections.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/DiscreteCategory.v b/theories/Categories/DiscreteCategory.v index 60e2c94af7e..269018bece4 100644 --- a/theories/Categories/DiscreteCategory.v +++ b/theories/Categories/DiscreteCategory.v @@ -4,7 +4,8 @@ Require Import HoTT.Basics GroupoidCategory.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (** A discrete category is a groupoid which is a 0-type *) Module Export Core. diff --git a/theories/Categories/DualFunctor.v b/theories/Categories/DualFunctor.v index d5a36d990b4..b1a0d876daa 100644 --- a/theories/Categories/DualFunctor.v +++ b/theories/Categories/DualFunctor.v @@ -8,7 +8,8 @@ Require Import Basics.Trunc Types.Sigma HoTT.Tactics Types.Forall. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/ExponentialLaws/Law0.v b/theories/Categories/ExponentialLaws/Law0.v index e6704a81a85..8842565dd19 100644 --- a/theories/Categories/ExponentialLaws/Law0.v +++ b/theories/Categories/ExponentialLaws/Law0.v @@ -6,7 +6,8 @@ Require Import HoTT.Basics HoTT.Types. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law1/Functors.v b/theories/Categories/ExponentialLaws/Law1/Functors.v index 4cf798facb1..c3aafebdde8 100644 --- a/theories/Categories/ExponentialLaws/Law1/Functors.v +++ b/theories/Categories/ExponentialLaws/Law1/Functors.v @@ -6,7 +6,8 @@ Require Import HoTT.Basics HoTT.Types. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law1/Law.v b/theories/Categories/ExponentialLaws/Law1/Law.v index 8ce178f1699..19223504ebe 100644 --- a/theories/Categories/ExponentialLaws/Law1/Law.v +++ b/theories/Categories/ExponentialLaws/Law1/Law.v @@ -7,7 +7,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law2/Functors.v b/theories/Categories/ExponentialLaws/Law2/Functors.v index 5d10cc5859c..819c08c32d1 100644 --- a/theories/Categories/ExponentialLaws/Law2/Functors.v +++ b/theories/Categories/ExponentialLaws/Law2/Functors.v @@ -4,7 +4,8 @@ Require Import Functor.Core FunctorCategory.Core Functor.Identity NaturalTransfo Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law2/Law.v b/theories/Categories/ExponentialLaws/Law2/Law.v index 169938590e7..bb4a929c2b1 100644 --- a/theories/Categories/ExponentialLaws/Law2/Law.v +++ b/theories/Categories/ExponentialLaws/Law2/Law.v @@ -9,7 +9,8 @@ Require Import ExponentialLaws.Law2.Functors. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law3/Functors.v b/theories/Categories/ExponentialLaws/Law3/Functors.v index 2fc051b6398..035e56c4a83 100644 --- a/theories/Categories/ExponentialLaws/Law3/Functors.v +++ b/theories/Categories/ExponentialLaws/Law3/Functors.v @@ -6,7 +6,8 @@ Require Import Types.Prod. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law3/Law.v b/theories/Categories/ExponentialLaws/Law3/Law.v index 7eac2c714c2..40ebae8501c 100644 --- a/theories/Categories/ExponentialLaws/Law3/Law.v +++ b/theories/Categories/ExponentialLaws/Law3/Law.v @@ -9,7 +9,8 @@ Require Import Types.Prod ExponentialLaws.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law4/Functors.v b/theories/Categories/ExponentialLaws/Law4/Functors.v index ca7fe035696..31ef5baed0b 100644 --- a/theories/Categories/ExponentialLaws/Law4/Functors.v +++ b/theories/Categories/ExponentialLaws/Law4/Functors.v @@ -5,7 +5,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law4/Law.v b/theories/Categories/ExponentialLaws/Law4/Law.v index b957d2d2de8..6500f10f5a5 100644 --- a/theories/Categories/ExponentialLaws/Law4/Law.v +++ b/theories/Categories/ExponentialLaws/Law4/Law.v @@ -8,7 +8,8 @@ Require Import ExponentialLaws.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/Functor/Attributes.v b/theories/Categories/Functor/Attributes.v index 209c054ee4f..a94930fe072 100644 --- a/theories/Categories/Functor/Attributes.v +++ b/theories/Categories/Functor/Attributes.v @@ -5,7 +5,8 @@ Require Import Basics.Trunc Types.Universe HIT.iso HoTT.Truncations.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/Functor/Composition/Core.v b/theories/Categories/Functor/Composition/Core.v index ef8848e973e..52799394534 100644 --- a/theories/Categories/Functor/Composition/Core.v +++ b/theories/Categories/Functor/Composition/Core.v @@ -4,7 +4,8 @@ Require Import Category.Core Functor.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Functor/Composition/Functorial/Attributes.v b/theories/Categories/Functor/Composition/Functorial/Attributes.v index be9802e05dc..f3a8d7c895c 100644 --- a/theories/Categories/Functor/Composition/Functorial/Attributes.v +++ b/theories/Categories/Functor/Composition/Functorial/Attributes.v @@ -12,7 +12,8 @@ Require Import HoTT.Truncations.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/Functor/Composition/Functorial/Core.v b/theories/Categories/Functor/Composition/Functorial/Core.v index 1dceced2fed..f0b54f04502 100644 --- a/theories/Categories/Functor/Composition/Functorial/Core.v +++ b/theories/Categories/Functor/Composition/Functorial/Core.v @@ -8,7 +8,8 @@ Require ProductLaws. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (** Construction of the functor [_∘_ : (C → D) × (D → E) → (C → E)] and its curried variant *) Section functorial_composition. diff --git a/theories/Categories/Functor/Composition/Laws.v b/theories/Categories/Functor/Composition/Laws.v index 90231b59249..293b3b4856d 100644 --- a/theories/Categories/Functor/Composition/Laws.v +++ b/theories/Categories/Functor/Composition/Laws.v @@ -6,7 +6,8 @@ Require Import Basics.PathGroupoids Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Functor/Core.v b/theories/Categories/Functor/Core.v index ac90a126dde..3a6c7da111c 100644 --- a/theories/Categories/Functor/Core.v +++ b/theories/Categories/Functor/Core.v @@ -4,7 +4,8 @@ Require Import Category.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Declare Scope functor_scope. Delimit Scope functor_scope with functor. diff --git a/theories/Categories/Functor/Dual.v b/theories/Categories/Functor/Dual.v index f7f73df5a08..6e21929e5a3 100644 --- a/theories/Categories/Functor/Dual.v +++ b/theories/Categories/Functor/Dual.v @@ -6,7 +6,8 @@ Require Import Category.Core Functor.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/Functor/Identity.v b/theories/Categories/Functor/Identity.v index f823512ade1..bdef196977e 100644 --- a/theories/Categories/Functor/Identity.v +++ b/theories/Categories/Functor/Identity.v @@ -4,7 +4,8 @@ Require Import Category.Core Functor.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Section identity. (** There is an identity functor. It does the obvious thing. *) diff --git a/theories/Categories/Functor/Paths.v b/theories/Categories/Functor/Paths.v index 18503710d5e..8b4e14df4e5 100644 --- a/theories/Categories/Functor/Paths.v +++ b/theories/Categories/Functor/Paths.v @@ -5,7 +5,8 @@ Require Import HoTT.Basics HoTT.Types HoTT.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Functor/Pointwise/Core.v b/theories/Categories/Functor/Pointwise/Core.v index 2d94a02a6c0..628f03429fc 100644 --- a/theories/Categories/Functor/Pointwise/Core.v +++ b/theories/Categories/Functor/Pointwise/Core.v @@ -4,7 +4,8 @@ Require Import Category.Core Functor.Core FunctorCategory.Core NaturalTransforma Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Functor/Pointwise/Properties.v b/theories/Categories/Functor/Pointwise/Properties.v index 64407740b85..6178c19aad7 100644 --- a/theories/Categories/Functor/Pointwise/Properties.v +++ b/theories/Categories/Functor/Pointwise/Properties.v @@ -6,7 +6,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope functor_scope. diff --git a/theories/Categories/Functor/Prod/Core.v b/theories/Categories/Functor/Prod/Core.v index bb3e703d5ea..878cac845b5 100644 --- a/theories/Categories/Functor/Prod/Core.v +++ b/theories/Categories/Functor/Prod/Core.v @@ -5,7 +5,8 @@ Require Import Types.Prod. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Notation fst_type := fst. Local Notation snd_type := snd. diff --git a/theories/Categories/Functor/Prod/Functorial.v b/theories/Categories/Functor/Prod/Functorial.v index 26a898e5f99..e1f99972614 100644 --- a/theories/Categories/Functor/Prod/Functorial.v +++ b/theories/Categories/Functor/Prod/Functorial.v @@ -5,7 +5,8 @@ Require Import NaturalTransformation.Paths. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/Functor/Prod/Universal.v b/theories/Categories/Functor/Prod/Universal.v index df1ad2d92e0..6d97a302903 100644 --- a/theories/Categories/Functor/Prod/Universal.v +++ b/theories/Categories/Functor/Prod/Universal.v @@ -7,7 +7,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Notation fst_type := Basics.Overture.fst. Local Notation snd_type := Basics.Overture.snd. diff --git a/theories/Categories/Functor/Sum.v b/theories/Categories/Functor/Sum.v index 7f90d0905b8..0e1e8b14079 100644 --- a/theories/Categories/Functor/Sum.v +++ b/theories/Categories/Functor/Sum.v @@ -6,7 +6,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (** We save [inl] and [inr] so we can use them to refer to the functors, too. Outside of the [Categories/] directory, they should always be referred to as [Functor.inl] and [Functor.inr], after a [Require Functor]. Outside of this file, but in the [Categories/] directory, if you do not want to depend on all of [Functor] (for e.g., speed reasons), they should be referred to as [Functor.Sum.inl] and [Functor.Sum.inr] after a [Require Functor.Sum]. *) Local Notation type_inl := inl. diff --git a/theories/Categories/FunctorCategory/Core.v b/theories/Categories/FunctorCategory/Core.v index 15896afa5d5..6a1323eb68e 100644 --- a/theories/Categories/FunctorCategory/Core.v +++ b/theories/Categories/FunctorCategory/Core.v @@ -6,7 +6,8 @@ Require Import NaturalTransformation.Composition.Core NaturalTransformation.Iden Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (** ** Definition of [C → D] *) Section functor_category. diff --git a/theories/Categories/FunctorCategory/Dual.v b/theories/Categories/FunctorCategory/Dual.v index 10e6623164f..06db58b564b 100644 --- a/theories/Categories/FunctorCategory/Dual.v +++ b/theories/Categories/FunctorCategory/Dual.v @@ -9,7 +9,8 @@ Require Import HoTT.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/FunctorCategory/Functorial.v b/theories/Categories/FunctorCategory/Functorial.v index 51f61031370..101d3feac97 100644 --- a/theories/Categories/FunctorCategory/Functorial.v +++ b/theories/Categories/FunctorCategory/Functorial.v @@ -4,7 +4,8 @@ Require Import Category.Core Functor.Core FunctorCategory.Core Functor.Pointwise Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope type_scope. diff --git a/theories/Categories/FunctorCategory/Morphisms.v b/theories/Categories/FunctorCategory/Morphisms.v index 396dfee5e29..7bd881d1e07 100644 --- a/theories/Categories/FunctorCategory/Morphisms.v +++ b/theories/Categories/FunctorCategory/Morphisms.v @@ -5,7 +5,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope category_scope. diff --git a/theories/Categories/FundamentalPreGroupoidCategory.v b/theories/Categories/FundamentalPreGroupoidCategory.v index c2cbfa69c69..dca017d67cc 100644 --- a/theories/Categories/FundamentalPreGroupoidCategory.v +++ b/theories/Categories/FundamentalPreGroupoidCategory.v @@ -6,7 +6,8 @@ Require Import HoTT.Basics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. diff --git a/theories/Categories/Grothendieck/PseudofunctorToCat.v b/theories/Categories/Grothendieck/PseudofunctorToCat.v index 973cc743077..6271de4c7a0 100644 --- a/theories/Categories/Grothendieck/PseudofunctorToCat.v +++ b/theories/Categories/Grothendieck/PseudofunctorToCat.v @@ -11,7 +11,8 @@ From HoTT Require Import Basics Types Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Grothendieck/ToCat.v b/theories/Categories/Grothendieck/ToCat.v index 839a13ed1f6..3de754da3f5 100644 --- a/theories/Categories/Grothendieck/ToCat.v +++ b/theories/Categories/Grothendieck/ToCat.v @@ -7,7 +7,8 @@ Require Import Grothendieck.PseudofunctorToCat. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Grothendieck/ToSet/Core.v b/theories/Categories/Grothendieck/ToSet/Core.v index 2182f73f99f..dc348291dd6 100644 --- a/theories/Categories/Grothendieck/ToSet/Core.v +++ b/theories/Categories/Grothendieck/ToSet/Core.v @@ -7,7 +7,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Grothendieck/ToSet/Morphisms.v b/theories/Categories/Grothendieck/ToSet/Morphisms.v index 384a2ebbfc0..33b0b16bb94 100644 --- a/theories/Categories/Grothendieck/ToSet/Morphisms.v +++ b/theories/Categories/Grothendieck/ToSet/Morphisms.v @@ -8,7 +8,8 @@ Require Import HoTT.Basics HoTT.Types. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Grothendieck/ToSet/Univalent.v b/theories/Categories/Grothendieck/ToSet/Univalent.v index 315a6a90032..17b69ccd212 100644 --- a/theories/Categories/Grothendieck/ToSet/Univalent.v +++ b/theories/Categories/Grothendieck/ToSet/Univalent.v @@ -10,7 +10,8 @@ Require Import HoTT.Types.Universe HoTT.Types.Sigma. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/GroupoidCategory/Core.v b/theories/Categories/GroupoidCategory/Core.v index d9311baf79e..fecf5d1f02c 100644 --- a/theories/Categories/GroupoidCategory/Core.v +++ b/theories/Categories/GroupoidCategory/Core.v @@ -5,7 +5,8 @@ Require Import Trunc PathGroupoids Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/GroupoidCategory/Dual.v b/theories/Categories/GroupoidCategory/Dual.v index 12e1594e9c0..b4a63070cc4 100644 --- a/theories/Categories/GroupoidCategory/Dual.v +++ b/theories/Categories/GroupoidCategory/Dual.v @@ -6,7 +6,8 @@ Require Import Basics.Trunc Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/GroupoidCategory/Morphisms.v b/theories/Categories/GroupoidCategory/Morphisms.v index 2ac89620538..140897b4199 100644 --- a/theories/Categories/GroupoidCategory/Morphisms.v +++ b/theories/Categories/GroupoidCategory/Morphisms.v @@ -5,7 +5,8 @@ Require Import Trunc Equivalences HoTT.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/HomFunctor.v b/theories/Categories/HomFunctor.v index 18f75e0b9e4..2d3cec9f9b6 100644 --- a/theories/Categories/HomFunctor.v +++ b/theories/Categories/HomFunctor.v @@ -7,7 +7,8 @@ Require Import Basics.Trunc. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/HomotopyPreCategory.v b/theories/Categories/HomotopyPreCategory.v index c125dc3f66c..05a9df0711e 100644 --- a/theories/Categories/HomotopyPreCategory.v +++ b/theories/Categories/HomotopyPreCategory.v @@ -5,7 +5,8 @@ Require Import HoTT.Basics HoTT.Truncations.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. diff --git a/theories/Categories/IndiscreteCategory.v b/theories/Categories/IndiscreteCategory.v index 61814188941..703a80b9406 100644 --- a/theories/Categories/IndiscreteCategory.v +++ b/theories/Categories/IndiscreteCategory.v @@ -5,7 +5,8 @@ Require Import Types.Unit Trunc HoTT.Tactics Equivalences. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (** ** Definition of an indiscrete category *) Module Export Core. diff --git a/theories/Categories/InitialTerminalCategory/Core.v b/theories/Categories/InitialTerminalCategory/Core.v index 11ca76691e8..23e90219815 100644 --- a/theories/Categories/InitialTerminalCategory/Core.v +++ b/theories/Categories/InitialTerminalCategory/Core.v @@ -6,7 +6,8 @@ Require Import NatCategory. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Unset Primitive Projections. (* suppress a warning about [IsTerminalCategory] *) Notation initial_category := (nat_category 0) (only parsing). diff --git a/theories/Categories/InitialTerminalCategory/Functors.v b/theories/Categories/InitialTerminalCategory/Functors.v index bafaeae0bc0..65cb971989e 100644 --- a/theories/Categories/InitialTerminalCategory/Functors.v +++ b/theories/Categories/InitialTerminalCategory/Functors.v @@ -7,7 +7,8 @@ Require Import HoTT.Basics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Section functors. Variable C : PreCategory. diff --git a/theories/Categories/InitialTerminalCategory/NaturalTransformations.v b/theories/Categories/InitialTerminalCategory/NaturalTransformations.v index f10cbaace7e..35b518d3900 100644 --- a/theories/Categories/InitialTerminalCategory/NaturalTransformations.v +++ b/theories/Categories/InitialTerminalCategory/NaturalTransformations.v @@ -6,7 +6,8 @@ Require Import Contractible. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Section NaturalTransformations. Variable C : PreCategory. diff --git a/theories/Categories/InitialTerminalCategory/Pseudofunctors.v b/theories/Categories/InitialTerminalCategory/Pseudofunctors.v index 6b49f564184..0f03a3c6dc3 100644 --- a/theories/Categories/InitialTerminalCategory/Pseudofunctors.v +++ b/theories/Categories/InitialTerminalCategory/Pseudofunctors.v @@ -11,7 +11,8 @@ Require Import PathGroupoids. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Section pseudofunctors. (** ** Constant functor from any terminal category *) diff --git a/theories/Categories/KanExtensions/Core.v b/theories/Categories/KanExtensions/Core.v index 88730968152..fe0805bf057 100644 --- a/theories/Categories/KanExtensions/Core.v +++ b/theories/Categories/KanExtensions/Core.v @@ -7,7 +7,8 @@ Require Import UniversalProperties. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/KanExtensions/Functors.v b/theories/Categories/KanExtensions/Functors.v index 996045f6e6f..b72623b086a 100644 --- a/theories/Categories/KanExtensions/Functors.v +++ b/theories/Categories/KanExtensions/Functors.v @@ -8,7 +8,8 @@ Require Import Adjoint.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Section kan_extension_functors. Context `{Funext}. diff --git a/theories/Categories/LaxComma/Core.v b/theories/Categories/LaxComma/Core.v index 1c5ffbe6601..ec9f5d744aa 100644 --- a/theories/Categories/LaxComma/Core.v +++ b/theories/Categories/LaxComma/Core.v @@ -16,7 +16,8 @@ Import LaxComma.CoreLaws.LaxCommaCategory. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/LaxComma/CoreLaws.v b/theories/Categories/LaxComma/CoreLaws.v index 9acd60b351f..30ba217a0bc 100644 --- a/theories/Categories/LaxComma/CoreLaws.v +++ b/theories/Categories/LaxComma/CoreLaws.v @@ -14,7 +14,8 @@ Import Functor.Identity.FunctorIdentityNotations. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/LaxComma/CoreParts.v b/theories/Categories/LaxComma/CoreParts.v index 399d1d93cfa..e4009ebd26b 100644 --- a/theories/Categories/LaxComma/CoreParts.v +++ b/theories/Categories/LaxComma/CoreParts.v @@ -12,7 +12,8 @@ Import Functor.Identity.FunctorIdentityNotations. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Limits/Core.v b/theories/Categories/Limits/Core.v index a0defc270ed..aa65452075a 100644 --- a/theories/Categories/Limits/Core.v +++ b/theories/Categories/Limits/Core.v @@ -11,7 +11,8 @@ Local Set Warnings "notation-overridden". Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/Limits/Functors.v b/theories/Categories/Limits/Functors.v index 736b2dfcdcf..8090e7dd3c8 100644 --- a/theories/Categories/Limits/Functors.v +++ b/theories/Categories/Limits/Functors.v @@ -9,7 +9,8 @@ Require Import NatCategory. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (** (co)limits assemble into functors *) diff --git a/theories/Categories/Monoidal/MonoidalCategory.v b/theories/Categories/Monoidal/MonoidalCategory.v index 3dd7cc345be..174929eaefe 100644 --- a/theories/Categories/Monoidal/MonoidalCategory.v +++ b/theories/Categories/Monoidal/MonoidalCategory.v @@ -9,7 +9,8 @@ Require Import ProductLaws. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Section MonoidalStructure. Context `{Funext}. diff --git a/theories/Categories/NatCategory.v b/theories/Categories/NatCategory.v index fcb9c47dacb..898d31803a7 100644 --- a/theories/Categories/NatCategory.v +++ b/theories/Categories/NatCategory.v @@ -6,7 +6,8 @@ Require Import Basics.Nat. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope nat_scope. Module Export Core. diff --git a/theories/Categories/NaturalTransformation/Composition/Core.v b/theories/Categories/NaturalTransformation/Composition/Core.v index b5b867f0272..48f1dccd416 100644 --- a/theories/Categories/NaturalTransformation/Composition/Core.v +++ b/theories/Categories/NaturalTransformation/Composition/Core.v @@ -4,7 +4,8 @@ Require Import Category.Core Functor.Core Functor.Composition.Core NaturalTransf Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/NaturalTransformation/Composition/Functorial.v b/theories/Categories/NaturalTransformation/Composition/Functorial.v index b914bd3b6da..6bd38ec72ca 100644 --- a/theories/Categories/NaturalTransformation/Composition/Functorial.v +++ b/theories/Categories/NaturalTransformation/Composition/Functorial.v @@ -5,7 +5,8 @@ Require Import FunctorCategory.Core Functor.Composition.Core NaturalTransformati Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/NaturalTransformation/Composition/Laws.v b/theories/Categories/NaturalTransformation/Composition/Laws.v index 152fb81c0e2..c04345f513a 100644 --- a/theories/Categories/NaturalTransformation/Composition/Laws.v +++ b/theories/Categories/NaturalTransformation/Composition/Laws.v @@ -4,7 +4,8 @@ Require Import Category.Core Functor.Core Functor.Identity Functor.Composition.C Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/NaturalTransformation/Core.v b/theories/Categories/NaturalTransformation/Core.v index 5a03a059bab..1929f5da485 100644 --- a/theories/Categories/NaturalTransformation/Core.v +++ b/theories/Categories/NaturalTransformation/Core.v @@ -4,7 +4,8 @@ Require Import Category.Core Functor.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Declare Scope natural_transformation_scope. Delimit Scope natural_transformation_scope with natural_transformation. diff --git a/theories/Categories/NaturalTransformation/Dual.v b/theories/Categories/NaturalTransformation/Dual.v index f88ae049fbe..9962737565b 100644 --- a/theories/Categories/NaturalTransformation/Dual.v +++ b/theories/Categories/NaturalTransformation/Dual.v @@ -6,7 +6,8 @@ Require Import Category.Core Functor.Core NaturalTransformation.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/NaturalTransformation/Identity.v b/theories/Categories/NaturalTransformation/Identity.v index 47725b2ae51..9917869a743 100644 --- a/theories/Categories/NaturalTransformation/Identity.v +++ b/theories/Categories/NaturalTransformation/Identity.v @@ -4,7 +4,8 @@ Require Import Category.Core Functor.Core NaturalTransformation.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope path_scope. diff --git a/theories/Categories/NaturalTransformation/Isomorphisms.v b/theories/Categories/NaturalTransformation/Isomorphisms.v index 51bbb64cd5b..d870399a9dd 100644 --- a/theories/Categories/NaturalTransformation/Isomorphisms.v +++ b/theories/Categories/NaturalTransformation/Isomorphisms.v @@ -10,7 +10,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/NaturalTransformation/Paths.v b/theories/Categories/NaturalTransformation/Paths.v index 550d734ce59..7a305abc381 100644 --- a/theories/Categories/NaturalTransformation/Paths.v +++ b/theories/Categories/NaturalTransformation/Paths.v @@ -5,7 +5,8 @@ Require Import Equivalences HoTT.Types Trunc Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/NaturalTransformation/Pointwise.v b/theories/Categories/NaturalTransformation/Pointwise.v index 8f6e5831888..5531e9aea3b 100644 --- a/theories/Categories/NaturalTransformation/Pointwise.v +++ b/theories/Categories/NaturalTransformation/Pointwise.v @@ -6,7 +6,8 @@ Require Import Functor.Pointwise.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (** Recall that a "pointwise" functor is a functor [Aᴮ → Cᴰ] induced by functors [D → B] and [A → C]. Given two functors [D → B] and a diff --git a/theories/Categories/NaturalTransformation/Prod.v b/theories/Categories/NaturalTransformation/Prod.v index 8da27e13676..52c5551040a 100644 --- a/theories/Categories/NaturalTransformation/Prod.v +++ b/theories/Categories/NaturalTransformation/Prod.v @@ -5,7 +5,8 @@ Require Import Types.Prod. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. (** ** Product of natural transformations *) Section prod. diff --git a/theories/Categories/NaturalTransformation/Sum.v b/theories/Categories/NaturalTransformation/Sum.v index 10a77278de3..50a79ddafe6 100644 --- a/theories/Categories/NaturalTransformation/Sum.v +++ b/theories/Categories/NaturalTransformation/Sum.v @@ -4,7 +4,8 @@ Require Import Category.Sum Functor.Sum NaturalTransformation.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Section sum. Definition sum diff --git a/theories/Categories/ProductLaws.v b/theories/Categories/ProductLaws.v index 6a62b0168ba..75af90b6b3f 100644 --- a/theories/Categories/ProductLaws.v +++ b/theories/Categories/ProductLaws.v @@ -5,7 +5,8 @@ Require Import Category.Core Functor.Core InitialTerminalCategory.Core InitialTe Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope functor_scope. diff --git a/theories/Categories/Profunctor/Core.v b/theories/Categories/Profunctor/Core.v index fd2c1f5cd55..fb493307a23 100644 --- a/theories/Categories/Profunctor/Core.v +++ b/theories/Categories/Profunctor/Core.v @@ -4,7 +4,8 @@ Require Import Category.Core Functor.Core Category.Prod Category.Dual SetCategor Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Declare Scope profunctor_scope. Delimit Scope profunctor_scope with profunctor. diff --git a/theories/Categories/Profunctor/Identity.v b/theories/Categories/Profunctor/Identity.v index 8b5e4426b37..714c75667ea 100644 --- a/theories/Categories/Profunctor/Identity.v +++ b/theories/Categories/Profunctor/Identity.v @@ -4,7 +4,8 @@ Require Import Category.Core Profunctor.Core HomFunctor. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope profunctor_scope. diff --git a/theories/Categories/Profunctor/Representable.v b/theories/Categories/Profunctor/Representable.v index 4d3145b0b42..82c0c7d095a 100644 --- a/theories/Categories/Profunctor/Representable.v +++ b/theories/Categories/Profunctor/Representable.v @@ -4,7 +4,8 @@ Require Import Category.Core Functor.Core Functor.Prod.Core Profunctor.Core Func Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. Local Open Scope profunctor_scope. diff --git a/theories/Categories/Pseudofunctor/Core.v b/theories/Categories/Pseudofunctor/Core.v index 3fe4af3dea6..77e35624dda 100644 --- a/theories/Categories/Pseudofunctor/Core.v +++ b/theories/Categories/Pseudofunctor/Core.v @@ -8,7 +8,8 @@ Require Import FunctorCategory.Core. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Pseudofunctor/FromFunctor.v b/theories/Categories/Pseudofunctor/FromFunctor.v index 65281cf542a..afb1773708e 100644 --- a/theories/Categories/Pseudofunctor/FromFunctor.v +++ b/theories/Categories/Pseudofunctor/FromFunctor.v @@ -12,7 +12,8 @@ Require Import Basics.PathGroupoids Basics.Trunc. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Pseudofunctor/Identity.v b/theories/Categories/Pseudofunctor/Identity.v index 36c81072e08..822cc32b85c 100644 --- a/theories/Categories/Pseudofunctor/Identity.v +++ b/theories/Categories/Pseudofunctor/Identity.v @@ -17,7 +17,8 @@ Require Import PathGroupoids. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/Pseudofunctor/RewriteLaws.v b/theories/Categories/Pseudofunctor/RewriteLaws.v index 767cf2cd4b0..020cf9c36c1 100644 --- a/theories/Categories/Pseudofunctor/RewriteLaws.v +++ b/theories/Categories/Pseudofunctor/RewriteLaws.v @@ -12,7 +12,8 @@ Require Import HoTT.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/PseudonaturalTransformation/Core.v b/theories/Categories/PseudonaturalTransformation/Core.v index 4db9628e73d..666f7d50c94 100644 --- a/theories/Categories/PseudonaturalTransformation/Core.v +++ b/theories/Categories/PseudonaturalTransformation/Core.v @@ -9,7 +9,8 @@ Require Import NaturalTransformation.Identity. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Declare Scope pseudonatural_transformation_scope. Delimit Scope pseudonatural_transformation_scope with pseudonatural_transformation. diff --git a/theories/Categories/SemiSimplicialSets.v b/theories/Categories/SemiSimplicialSets.v index 7e54de20954..d65222cb034 100644 --- a/theories/Categories/SemiSimplicialSets.v +++ b/theories/Categories/SemiSimplicialSets.v @@ -10,7 +10,8 @@ Require Import Category.Sigma.OnMorphisms Category.Subcategory.Wide. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/SetCategory/Core.v b/theories/Categories/SetCategory/Core.v index cd2fb4838fd..862394655c8 100644 --- a/theories/Categories/SetCategory/Core.v +++ b/theories/Categories/SetCategory/Core.v @@ -5,7 +5,8 @@ Require Import HoTT.Basics HoTT.Types TruncType. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Notation cat_of obj := (@Build_PreCategory obj diff --git a/theories/Categories/SetCategory/Functors/SetProp.v b/theories/Categories/SetCategory/Functors/SetProp.v index 080bfe25c44..cdf46c60981 100644 --- a/theories/Categories/SetCategory/Functors/SetProp.v +++ b/theories/Categories/SetCategory/Functors/SetProp.v @@ -5,7 +5,8 @@ Require Import Basics.Trunc. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Section set_coercions_definitions. Context `{Funext}. diff --git a/theories/Categories/SetCategory/Morphisms.v b/theories/Categories/SetCategory/Morphisms.v index 9007087bc56..d6cef2227a3 100644 --- a/theories/Categories/SetCategory/Morphisms.v +++ b/theories/Categories/SetCategory/Morphisms.v @@ -8,7 +8,8 @@ Require Import HoTT.Basics HoTT.Types TruncType. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. diff --git a/theories/Categories/SimplicialSets.v b/theories/Categories/SimplicialSets.v index 3a7dce5c228..edd1cc49390 100644 --- a/theories/Categories/SimplicialSets.v +++ b/theories/Categories/SimplicialSets.v @@ -9,7 +9,8 @@ Require Import Functor.Identity Functor.Composition.Core Functor.Composition.Law Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. Local Open Scope category_scope. diff --git a/theories/Categories/Structure/Core.v b/theories/Categories/Structure/Core.v index 1d5d6ed904d..ad0994abc62 100644 --- a/theories/Categories/Structure/Core.v +++ b/theories/Categories/Structure/Core.v @@ -5,7 +5,8 @@ Require Import HoTT.Basics HoTT.Types HSet. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Structure/IdentityPrinciple.v b/theories/Categories/Structure/IdentityPrinciple.v index c6c2397c923..915df617623 100644 --- a/theories/Categories/Structure/IdentityPrinciple.v +++ b/theories/Categories/Structure/IdentityPrinciple.v @@ -7,7 +7,8 @@ Require Import Basics.Iff Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope category_scope. diff --git a/theories/Categories/UniversalProperties.v b/theories/Categories/UniversalProperties.v index 390852f4950..6c2d68aac60 100644 --- a/theories/Categories/UniversalProperties.v +++ b/theories/Categories/UniversalProperties.v @@ -13,7 +13,8 @@ Require Import Basics.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Yoneda.v b/theories/Categories/Yoneda.v index c7d76f9578e..7709b99fed3 100644 --- a/theories/Categories/Yoneda.v +++ b/theories/Categories/Yoneda.v @@ -15,7 +15,8 @@ Require Import HoTT.Tactics. Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. -Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +Set Asymmetric Patterns. +#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope category_scope. From fa220fc3ba5cdb6ce7a7cb6f77dee8372e49ed1c Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 24 Apr 2026 14:17:45 +0000 Subject: [PATCH 2/2] Further style fixes: put warning attribute on its own line; add version comment in Settings.v Agent-Logs-Url: https://github.com/HoTT/Coq-HoTT/sessions/b1916f32-c0fb-4747-832d-a11a59fbf2aa Co-authored-by: Alizter <8614547+Alizter@users.noreply.github.com> --- theories/Basics/Settings.v | 4 +++- theories/Categories/Adjoint/Composition/AssociativityLaw.v | 3 ++- theories/Categories/Adjoint/Composition/Core.v | 3 ++- theories/Categories/Adjoint/Composition/IdentityLaws.v | 3 ++- theories/Categories/Adjoint/Composition/LawsTactic.v | 3 ++- theories/Categories/Adjoint/Dual.v | 3 ++- theories/Categories/Adjoint/Functorial/Core.v | 3 ++- theories/Categories/Adjoint/Functorial/Laws.v | 3 ++- theories/Categories/Adjoint/Functorial/Parts.v | 3 ++- theories/Categories/Adjoint/Hom.v | 3 ++- theories/Categories/Adjoint/HomCoercions.v | 3 ++- theories/Categories/Adjoint/Identity.v | 3 ++- theories/Categories/Adjoint/Paths.v | 3 ++- theories/Categories/Adjoint/Pointwise.v | 3 ++- theories/Categories/Adjoint/UnitCounit.v | 3 ++- theories/Categories/Adjoint/UnitCounitCoercions.v | 3 ++- theories/Categories/Adjoint/UniversalMorphisms/Core.v | 3 ++- theories/Categories/Cat/Core.v | 3 ++- theories/Categories/Cat/Morphisms.v | 3 ++- theories/Categories/Category/Core.v | 3 ++- theories/Categories/Category/Dual.v | 3 ++- theories/Categories/Category/Morphisms.v | 3 ++- theories/Categories/Category/Objects.v | 3 ++- theories/Categories/Category/Paths.v | 3 ++- theories/Categories/Category/Pi.v | 3 ++- theories/Categories/Category/Prod.v | 3 ++- theories/Categories/Category/Sigma/Core.v | 3 ++- theories/Categories/Category/Sigma/OnMorphisms.v | 3 ++- theories/Categories/Category/Sigma/OnObjects.v | 3 ++- theories/Categories/Category/Sigma/Univalent.v | 3 ++- theories/Categories/Category/Strict.v | 3 ++- theories/Categories/Category/Sum.v | 3 ++- theories/Categories/Category/Univalent.v | 3 ++- theories/Categories/CategoryOfGroupoids.v | 3 ++- theories/Categories/CategoryOfSections/Core.v | 3 ++- theories/Categories/ChainCategory.v | 3 ++- theories/Categories/Comma/Core.v | 3 ++- theories/Categories/Comma/Dual.v | 3 ++- theories/Categories/Comma/Functorial.v | 3 ++- theories/Categories/Comma/InducedFunctors.v | 3 ++- theories/Categories/Comma/Projection.v | 3 ++- theories/Categories/Comma/ProjectionFunctors.v | 3 ++- theories/Categories/DependentProduct.v | 3 ++- theories/Categories/DiscreteCategory.v | 3 ++- theories/Categories/DualFunctor.v | 3 ++- theories/Categories/ExponentialLaws/Law0.v | 3 ++- theories/Categories/ExponentialLaws/Law1/Functors.v | 3 ++- theories/Categories/ExponentialLaws/Law1/Law.v | 3 ++- theories/Categories/ExponentialLaws/Law2/Functors.v | 3 ++- theories/Categories/ExponentialLaws/Law2/Law.v | 3 ++- theories/Categories/ExponentialLaws/Law3/Functors.v | 3 ++- theories/Categories/ExponentialLaws/Law3/Law.v | 3 ++- theories/Categories/ExponentialLaws/Law4/Functors.v | 3 ++- theories/Categories/ExponentialLaws/Law4/Law.v | 3 ++- theories/Categories/Functor/Attributes.v | 3 ++- theories/Categories/Functor/Composition/Core.v | 3 ++- .../Categories/Functor/Composition/Functorial/Attributes.v | 3 ++- theories/Categories/Functor/Composition/Functorial/Core.v | 3 ++- theories/Categories/Functor/Composition/Laws.v | 3 ++- theories/Categories/Functor/Core.v | 3 ++- theories/Categories/Functor/Dual.v | 3 ++- theories/Categories/Functor/Identity.v | 3 ++- theories/Categories/Functor/Paths.v | 3 ++- theories/Categories/Functor/Pointwise/Core.v | 3 ++- theories/Categories/Functor/Pointwise/Properties.v | 3 ++- theories/Categories/Functor/Prod/Core.v | 3 ++- theories/Categories/Functor/Prod/Functorial.v | 3 ++- theories/Categories/Functor/Prod/Universal.v | 3 ++- theories/Categories/Functor/Sum.v | 3 ++- theories/Categories/FunctorCategory/Core.v | 3 ++- theories/Categories/FunctorCategory/Dual.v | 3 ++- theories/Categories/FunctorCategory/Functorial.v | 3 ++- theories/Categories/FunctorCategory/Morphisms.v | 3 ++- theories/Categories/FundamentalPreGroupoidCategory.v | 3 ++- theories/Categories/Grothendieck/PseudofunctorToCat.v | 3 ++- theories/Categories/Grothendieck/ToCat.v | 3 ++- theories/Categories/Grothendieck/ToSet/Core.v | 3 ++- theories/Categories/Grothendieck/ToSet/Morphisms.v | 3 ++- theories/Categories/Grothendieck/ToSet/Univalent.v | 3 ++- theories/Categories/GroupoidCategory/Core.v | 3 ++- theories/Categories/GroupoidCategory/Dual.v | 3 ++- theories/Categories/GroupoidCategory/Morphisms.v | 3 ++- theories/Categories/HomFunctor.v | 3 ++- theories/Categories/HomotopyPreCategory.v | 3 ++- theories/Categories/IndiscreteCategory.v | 3 ++- theories/Categories/InitialTerminalCategory/Core.v | 3 ++- theories/Categories/InitialTerminalCategory/Functors.v | 3 ++- .../InitialTerminalCategory/NaturalTransformations.v | 3 ++- theories/Categories/InitialTerminalCategory/Pseudofunctors.v | 3 ++- theories/Categories/KanExtensions/Core.v | 3 ++- theories/Categories/KanExtensions/Functors.v | 3 ++- theories/Categories/LaxComma/Core.v | 3 ++- theories/Categories/LaxComma/CoreLaws.v | 3 ++- theories/Categories/LaxComma/CoreParts.v | 3 ++- theories/Categories/Limits/Core.v | 3 ++- theories/Categories/Limits/Functors.v | 3 ++- theories/Categories/Monoidal/MonoidalCategory.v | 3 ++- theories/Categories/NatCategory.v | 3 ++- theories/Categories/NaturalTransformation/Composition/Core.v | 3 ++- .../Categories/NaturalTransformation/Composition/Functorial.v | 3 ++- theories/Categories/NaturalTransformation/Composition/Laws.v | 3 ++- theories/Categories/NaturalTransformation/Core.v | 3 ++- theories/Categories/NaturalTransformation/Dual.v | 3 ++- theories/Categories/NaturalTransformation/Identity.v | 3 ++- theories/Categories/NaturalTransformation/Isomorphisms.v | 3 ++- theories/Categories/NaturalTransformation/Paths.v | 3 ++- theories/Categories/NaturalTransformation/Pointwise.v | 3 ++- theories/Categories/NaturalTransformation/Prod.v | 3 ++- theories/Categories/NaturalTransformation/Sum.v | 3 ++- theories/Categories/ProductLaws.v | 3 ++- theories/Categories/Profunctor/Core.v | 3 ++- theories/Categories/Profunctor/Identity.v | 3 ++- theories/Categories/Profunctor/Representable.v | 3 ++- theories/Categories/Pseudofunctor/Core.v | 3 ++- theories/Categories/Pseudofunctor/FromFunctor.v | 3 ++- theories/Categories/Pseudofunctor/Identity.v | 3 ++- theories/Categories/Pseudofunctor/RewriteLaws.v | 3 ++- theories/Categories/PseudonaturalTransformation/Core.v | 3 ++- theories/Categories/SemiSimplicialSets.v | 3 ++- theories/Categories/SetCategory/Core.v | 3 ++- theories/Categories/SetCategory/Functors/SetProp.v | 3 ++- theories/Categories/SetCategory/Morphisms.v | 3 ++- theories/Categories/SimplicialSets.v | 3 ++- theories/Categories/Structure/Core.v | 3 ++- theories/Categories/Structure/IdentityPrinciple.v | 3 ++- theories/Categories/UniversalProperties.v | 3 ++- theories/Categories/Yoneda.v | 3 ++- 127 files changed, 255 insertions(+), 127 deletions(-) diff --git a/theories/Basics/Settings.v b/theories/Basics/Settings.v index e33cf0ea40d..2f895e2effd 100644 --- a/theories/Basics/Settings.v +++ b/theories/Basics/Settings.v @@ -43,7 +43,9 @@ Global Set Printing Primitive Projection Parameters. (** This flag removes parameters from constructors in patterns that appear in a match statement. *) Global Set Asymmetric Patterns. -#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits. +(** The warning clause here and in other parts of the library can be removed once our minimum Rocq version is 9.3. *) +#[warning="-unknown-option"] +Global Set Asymmetric Patterns No Implicits. (** ** Unification *) diff --git a/theories/Categories/Adjoint/Composition/AssociativityLaw.v b/theories/Categories/Adjoint/Composition/AssociativityLaw.v index bd4e1327026..decac5e8a85 100644 --- a/theories/Categories/Adjoint/Composition/AssociativityLaw.v +++ b/theories/Categories/Adjoint/Composition/AssociativityLaw.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope adjunction_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Composition/Core.v b/theories/Categories/Adjoint/Composition/Core.v index 5d5dc8e017c..7e4f0ed75b2 100644 --- a/theories/Categories/Adjoint/Composition/Core.v +++ b/theories/Categories/Adjoint/Composition/Core.v @@ -11,7 +11,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/Adjoint/Composition/IdentityLaws.v b/theories/Categories/Adjoint/Composition/IdentityLaws.v index 4bf5ab2b439..bab836b0010 100644 --- a/theories/Categories/Adjoint/Composition/IdentityLaws.v +++ b/theories/Categories/Adjoint/Composition/IdentityLaws.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope adjunction_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Composition/LawsTactic.v b/theories/Categories/Adjoint/Composition/LawsTactic.v index 1ebce444122..c6c3cdcb96e 100644 --- a/theories/Categories/Adjoint/Composition/LawsTactic.v +++ b/theories/Categories/Adjoint/Composition/LawsTactic.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Ltac law_t := rewrite !transport_path_prod'; simpl; diff --git a/theories/Categories/Adjoint/Dual.v b/theories/Categories/Adjoint/Dual.v index 4d132c6bab6..99af2b42fff 100644 --- a/theories/Categories/Adjoint/Dual.v +++ b/theories/Categories/Adjoint/Dual.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/Adjoint/Functorial/Core.v b/theories/Categories/Adjoint/Functorial/Core.v index 2429c5f3ccb..b6722981210 100644 --- a/theories/Categories/Adjoint/Functorial/Core.v +++ b/theories/Categories/Adjoint/Functorial/Core.v @@ -11,7 +11,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Functorial/Laws.v b/theories/Categories/Adjoint/Functorial/Laws.v index f2ed5ceeb31..d22f5187a17 100644 --- a/theories/Categories/Adjoint/Functorial/Laws.v +++ b/theories/Categories/Adjoint/Functorial/Laws.v @@ -14,7 +14,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Functorial/Parts.v b/theories/Categories/Adjoint/Functorial/Parts.v index 4982922b1ba..abfb7fd8243 100644 --- a/theories/Categories/Adjoint/Functorial/Parts.v +++ b/theories/Categories/Adjoint/Functorial/Parts.v @@ -9,7 +9,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Hom.v b/theories/Categories/Adjoint/Hom.v index 33e4ac11b0c..dbce1b3aa13 100644 --- a/theories/Categories/Adjoint/Hom.v +++ b/theories/Categories/Adjoint/Hom.v @@ -12,7 +12,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/HomCoercions.v b/theories/Categories/Adjoint/HomCoercions.v index b67958bc3f6..dea732fdf69 100644 --- a/theories/Categories/Adjoint/HomCoercions.v +++ b/theories/Categories/Adjoint/HomCoercions.v @@ -12,7 +12,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/Identity.v b/theories/Categories/Adjoint/Identity.v index dd45cde8130..355206469ad 100644 --- a/theories/Categories/Adjoint/Identity.v +++ b/theories/Categories/Adjoint/Identity.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Section identity. (** There is an identity adjunction. It does the obvious thing. *) diff --git a/theories/Categories/Adjoint/Paths.v b/theories/Categories/Adjoint/Paths.v index 959ba80b307..318415ebe18 100644 --- a/theories/Categories/Adjoint/Paths.v +++ b/theories/Categories/Adjoint/Paths.v @@ -9,7 +9,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/Adjoint/Pointwise.v b/theories/Categories/Adjoint/Pointwise.v index 0837ee6fa4c..21dc6f4d953 100644 --- a/theories/Categories/Adjoint/Pointwise.v +++ b/theories/Categories/Adjoint/Pointwise.v @@ -16,7 +16,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope functor_scope. diff --git a/theories/Categories/Adjoint/UnitCounit.v b/theories/Categories/Adjoint/UnitCounit.v index ecc31bd9696..1172991cd6e 100644 --- a/theories/Categories/Adjoint/UnitCounit.v +++ b/theories/Categories/Adjoint/UnitCounit.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Adjoint/UnitCounitCoercions.v b/theories/Categories/Adjoint/UnitCounitCoercions.v index 7a83ba42d93..a47f42999fa 100644 --- a/theories/Categories/Adjoint/UnitCounitCoercions.v +++ b/theories/Categories/Adjoint/UnitCounitCoercions.v @@ -9,7 +9,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope category_scope. diff --git a/theories/Categories/Adjoint/UniversalMorphisms/Core.v b/theories/Categories/Adjoint/UniversalMorphisms/Core.v index 4c023fc1dd9..224edbe875a 100644 --- a/theories/Categories/Adjoint/UniversalMorphisms/Core.v +++ b/theories/Categories/Adjoint/UniversalMorphisms/Core.v @@ -13,7 +13,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Cat/Core.v b/theories/Categories/Cat/Core.v index d9247f85fc3..a4a2a4e29b6 100644 --- a/theories/Categories/Cat/Core.v +++ b/theories/Categories/Cat/Core.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/Cat/Morphisms.v b/theories/Categories/Cat/Morphisms.v index 3db08a14def..fb6996a22a9 100644 --- a/theories/Categories/Cat/Morphisms.v +++ b/theories/Categories/Cat/Morphisms.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Core.v b/theories/Categories/Category/Core.v index 150213f8078..4b413b22c41 100644 --- a/theories/Categories/Category/Core.v +++ b/theories/Categories/Category/Core.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Declare Scope morphism_scope. Declare Scope category_scope. diff --git a/theories/Categories/Category/Dual.v b/theories/Categories/Category/Dual.v index b27d5c9ac82..8ef3725ff94 100644 --- a/theories/Categories/Category/Dual.v +++ b/theories/Categories/Category/Dual.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Morphisms.v b/theories/Categories/Category/Morphisms.v index 0df9de8058c..a0f00952ab1 100644 --- a/theories/Categories/Category/Morphisms.v +++ b/theories/Categories/Category/Morphisms.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Objects.v b/theories/Categories/Category/Objects.v index 36af18ea6e2..abc72a5e7ba 100644 --- a/theories/Categories/Category/Objects.v +++ b/theories/Categories/Category/Objects.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Paths.v b/theories/Categories/Category/Paths.v index ecad6e25d11..a89c19d7eab 100644 --- a/theories/Categories/Category/Paths.v +++ b/theories/Categories/Category/Paths.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope category_scope. diff --git a/theories/Categories/Category/Pi.v b/theories/Categories/Category/Pi.v index d384cd20a96..780220926cd 100644 --- a/theories/Categories/Category/Pi.v +++ b/theories/Categories/Category/Pi.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Prod.v b/theories/Categories/Category/Prod.v index 3aa5f104ec0..c8ba0658dd7 100644 --- a/theories/Categories/Category/Prod.v +++ b/theories/Categories/Category/Prod.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Sigma/Core.v b/theories/Categories/Category/Sigma/Core.v index d4e59db8353..74bb1cb7a27 100644 --- a/theories/Categories/Category/Sigma/Core.v +++ b/theories/Categories/Category/Sigma/Core.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Notation sig_type := sig. diff --git a/theories/Categories/Category/Sigma/OnMorphisms.v b/theories/Categories/Category/Sigma/OnMorphisms.v index 130c7408622..835f1e67f45 100644 --- a/theories/Categories/Category/Sigma/OnMorphisms.v +++ b/theories/Categories/Category/Sigma/OnMorphisms.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Notation sig_type := Overture.sig. Local Notation pr1_type := Overture.pr1. diff --git a/theories/Categories/Category/Sigma/OnObjects.v b/theories/Categories/Category/Sigma/OnObjects.v index 29d8833857d..848de599672 100644 --- a/theories/Categories/Category/Sigma/OnObjects.v +++ b/theories/Categories/Category/Sigma/OnObjects.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Notation sig_type := Overture.sig. Local Notation pr1_type := Overture.pr1. diff --git a/theories/Categories/Category/Sigma/Univalent.v b/theories/Categories/Category/Sigma/Univalent.v index 3e441951e49..4412f6fb699 100644 --- a/theories/Categories/Category/Sigma/Univalent.v +++ b/theories/Categories/Category/Sigma/Univalent.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Notation pr1_type := Overture.pr1 (only parsing). diff --git a/theories/Categories/Category/Strict.v b/theories/Categories/Category/Strict.v index 8244bb821ea..ef85361e797 100644 --- a/theories/Categories/Category/Strict.v +++ b/theories/Categories/Category/Strict.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Category/Sum.v b/theories/Categories/Category/Sum.v index c5c43566825..9de227d5f41 100644 --- a/theories/Categories/Category/Sum.v +++ b/theories/Categories/Category/Sum.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. (** ** Definition of [+] for categories *) Section internals. diff --git a/theories/Categories/Category/Univalent.v b/theories/Categories/Category/Univalent.v index 76fa6275fc0..950b0b6e22b 100644 --- a/theories/Categories/Category/Univalent.v +++ b/theories/Categories/Category/Univalent.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/CategoryOfGroupoids.v b/theories/Categories/CategoryOfGroupoids.v index f58fcc3305b..e66131d6c81 100644 --- a/theories/Categories/CategoryOfGroupoids.v +++ b/theories/Categories/CategoryOfGroupoids.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/CategoryOfSections/Core.v b/theories/Categories/CategoryOfSections/Core.v index 538432ccd5c..1e607d3b070 100644 --- a/theories/Categories/CategoryOfSections/Core.v +++ b/theories/Categories/CategoryOfSections/Core.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ChainCategory.v b/theories/Categories/ChainCategory.v index 70c9a7a0788..9642c0826af 100644 --- a/theories/Categories/ChainCategory.v +++ b/theories/Categories/ChainCategory.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope nat_scope. diff --git a/theories/Categories/Comma/Core.v b/theories/Categories/Comma/Core.v index c949bb55693..1e5f6681dd9 100644 --- a/theories/Categories/Comma/Core.v +++ b/theories/Categories/Comma/Core.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Comma/Dual.v b/theories/Categories/Comma/Dual.v index a76b4d37e75..bad79776e4f 100644 --- a/theories/Categories/Comma/Dual.v +++ b/theories/Categories/Comma/Dual.v @@ -11,7 +11,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Comma/Functorial.v b/theories/Categories/Comma/Functorial.v index 5bb00a58e1e..4a77516040f 100644 --- a/theories/Categories/Comma/Functorial.v +++ b/theories/Categories/Comma/Functorial.v @@ -15,7 +15,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Comma/InducedFunctors.v b/theories/Categories/Comma/InducedFunctors.v index 42e45ccad81..5441d1cec5e 100644 --- a/theories/Categories/Comma/InducedFunctors.v +++ b/theories/Categories/Comma/InducedFunctors.v @@ -16,7 +16,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. Local Open Scope category_scope. diff --git a/theories/Categories/Comma/Projection.v b/theories/Categories/Comma/Projection.v index d7b64470b0f..78f97655e5b 100644 --- a/theories/Categories/Comma/Projection.v +++ b/theories/Categories/Comma/Projection.v @@ -13,7 +13,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. Local Open Scope category_scope. diff --git a/theories/Categories/Comma/ProjectionFunctors.v b/theories/Categories/Comma/ProjectionFunctors.v index f239ff64d54..271590f400f 100644 --- a/theories/Categories/Comma/ProjectionFunctors.v +++ b/theories/Categories/Comma/ProjectionFunctors.v @@ -19,7 +19,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/DependentProduct.v b/theories/Categories/DependentProduct.v index d59e36b5310..a6e3d856ec1 100644 --- a/theories/Categories/DependentProduct.v +++ b/theories/Categories/DependentProduct.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/DiscreteCategory.v b/theories/Categories/DiscreteCategory.v index 269018bece4..2e10a6ae9e7 100644 --- a/theories/Categories/DiscreteCategory.v +++ b/theories/Categories/DiscreteCategory.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. (** A discrete category is a groupoid which is a 0-type *) Module Export Core. diff --git a/theories/Categories/DualFunctor.v b/theories/Categories/DualFunctor.v index b1a0d876daa..7f9775422a6 100644 --- a/theories/Categories/DualFunctor.v +++ b/theories/Categories/DualFunctor.v @@ -9,7 +9,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/ExponentialLaws/Law0.v b/theories/Categories/ExponentialLaws/Law0.v index 8842565dd19..1dfe7f33c5e 100644 --- a/theories/Categories/ExponentialLaws/Law0.v +++ b/theories/Categories/ExponentialLaws/Law0.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law1/Functors.v b/theories/Categories/ExponentialLaws/Law1/Functors.v index c3aafebdde8..9e41b3e9208 100644 --- a/theories/Categories/ExponentialLaws/Law1/Functors.v +++ b/theories/Categories/ExponentialLaws/Law1/Functors.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law1/Law.v b/theories/Categories/ExponentialLaws/Law1/Law.v index 19223504ebe..5e5193cf229 100644 --- a/theories/Categories/ExponentialLaws/Law1/Law.v +++ b/theories/Categories/ExponentialLaws/Law1/Law.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law2/Functors.v b/theories/Categories/ExponentialLaws/Law2/Functors.v index 819c08c32d1..b63b8e522d1 100644 --- a/theories/Categories/ExponentialLaws/Law2/Functors.v +++ b/theories/Categories/ExponentialLaws/Law2/Functors.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law2/Law.v b/theories/Categories/ExponentialLaws/Law2/Law.v index bb4a929c2b1..484d6d8cac5 100644 --- a/theories/Categories/ExponentialLaws/Law2/Law.v +++ b/theories/Categories/ExponentialLaws/Law2/Law.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law3/Functors.v b/theories/Categories/ExponentialLaws/Law3/Functors.v index 035e56c4a83..fe8ef14e325 100644 --- a/theories/Categories/ExponentialLaws/Law3/Functors.v +++ b/theories/Categories/ExponentialLaws/Law3/Functors.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law3/Law.v b/theories/Categories/ExponentialLaws/Law3/Law.v index 40ebae8501c..bfa05262ca7 100644 --- a/theories/Categories/ExponentialLaws/Law3/Law.v +++ b/theories/Categories/ExponentialLaws/Law3/Law.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law4/Functors.v b/theories/Categories/ExponentialLaws/Law4/Functors.v index 31ef5baed0b..14107106d7a 100644 --- a/theories/Categories/ExponentialLaws/Law4/Functors.v +++ b/theories/Categories/ExponentialLaws/Law4/Functors.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/ExponentialLaws/Law4/Law.v b/theories/Categories/ExponentialLaws/Law4/Law.v index 6500f10f5a5..0605ff9d19c 100644 --- a/theories/Categories/ExponentialLaws/Law4/Law.v +++ b/theories/Categories/ExponentialLaws/Law4/Law.v @@ -9,7 +9,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/Functor/Attributes.v b/theories/Categories/Functor/Attributes.v index a94930fe072..b4a20ec10c3 100644 --- a/theories/Categories/Functor/Attributes.v +++ b/theories/Categories/Functor/Attributes.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/Functor/Composition/Core.v b/theories/Categories/Functor/Composition/Core.v index 52799394534..eab48b66699 100644 --- a/theories/Categories/Functor/Composition/Core.v +++ b/theories/Categories/Functor/Composition/Core.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Functor/Composition/Functorial/Attributes.v b/theories/Categories/Functor/Composition/Functorial/Attributes.v index f3a8d7c895c..c9065145836 100644 --- a/theories/Categories/Functor/Composition/Functorial/Attributes.v +++ b/theories/Categories/Functor/Composition/Functorial/Attributes.v @@ -13,7 +13,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/Functor/Composition/Functorial/Core.v b/theories/Categories/Functor/Composition/Functorial/Core.v index f0b54f04502..62044d6dcd4 100644 --- a/theories/Categories/Functor/Composition/Functorial/Core.v +++ b/theories/Categories/Functor/Composition/Functorial/Core.v @@ -9,7 +9,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. (** Construction of the functor [_∘_ : (C → D) × (D → E) → (C → E)] and its curried variant *) Section functorial_composition. diff --git a/theories/Categories/Functor/Composition/Laws.v b/theories/Categories/Functor/Composition/Laws.v index 293b3b4856d..addcff84a6e 100644 --- a/theories/Categories/Functor/Composition/Laws.v +++ b/theories/Categories/Functor/Composition/Laws.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Functor/Core.v b/theories/Categories/Functor/Core.v index 3a6c7da111c..3662bb83bfa 100644 --- a/theories/Categories/Functor/Core.v +++ b/theories/Categories/Functor/Core.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Declare Scope functor_scope. Delimit Scope functor_scope with functor. diff --git a/theories/Categories/Functor/Dual.v b/theories/Categories/Functor/Dual.v index 6e21929e5a3..36676db4dd0 100644 --- a/theories/Categories/Functor/Dual.v +++ b/theories/Categories/Functor/Dual.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/Functor/Identity.v b/theories/Categories/Functor/Identity.v index bdef196977e..9116d16f639 100644 --- a/theories/Categories/Functor/Identity.v +++ b/theories/Categories/Functor/Identity.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Section identity. (** There is an identity functor. It does the obvious thing. *) diff --git a/theories/Categories/Functor/Paths.v b/theories/Categories/Functor/Paths.v index 8b4e14df4e5..79adb66b6a0 100644 --- a/theories/Categories/Functor/Paths.v +++ b/theories/Categories/Functor/Paths.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Functor/Pointwise/Core.v b/theories/Categories/Functor/Pointwise/Core.v index 628f03429fc..d55c28d2feb 100644 --- a/theories/Categories/Functor/Pointwise/Core.v +++ b/theories/Categories/Functor/Pointwise/Core.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Functor/Pointwise/Properties.v b/theories/Categories/Functor/Pointwise/Properties.v index 6178c19aad7..0fcde0bc2ff 100644 --- a/theories/Categories/Functor/Pointwise/Properties.v +++ b/theories/Categories/Functor/Pointwise/Properties.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope functor_scope. diff --git a/theories/Categories/Functor/Prod/Core.v b/theories/Categories/Functor/Prod/Core.v index 878cac845b5..4da1b230a7f 100644 --- a/theories/Categories/Functor/Prod/Core.v +++ b/theories/Categories/Functor/Prod/Core.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Notation fst_type := fst. Local Notation snd_type := snd. diff --git a/theories/Categories/Functor/Prod/Functorial.v b/theories/Categories/Functor/Prod/Functorial.v index e1f99972614..45a8579cc06 100644 --- a/theories/Categories/Functor/Prod/Functorial.v +++ b/theories/Categories/Functor/Prod/Functorial.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/Functor/Prod/Universal.v b/theories/Categories/Functor/Prod/Universal.v index 6d97a302903..6beb025b088 100644 --- a/theories/Categories/Functor/Prod/Universal.v +++ b/theories/Categories/Functor/Prod/Universal.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Notation fst_type := Basics.Overture.fst. Local Notation snd_type := Basics.Overture.snd. diff --git a/theories/Categories/Functor/Sum.v b/theories/Categories/Functor/Sum.v index 0e1e8b14079..7d58a047517 100644 --- a/theories/Categories/Functor/Sum.v +++ b/theories/Categories/Functor/Sum.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. (** We save [inl] and [inr] so we can use them to refer to the functors, too. Outside of the [Categories/] directory, they should always be referred to as [Functor.inl] and [Functor.inr], after a [Require Functor]. Outside of this file, but in the [Categories/] directory, if you do not want to depend on all of [Functor] (for e.g., speed reasons), they should be referred to as [Functor.Sum.inl] and [Functor.Sum.inr] after a [Require Functor.Sum]. *) Local Notation type_inl := inl. diff --git a/theories/Categories/FunctorCategory/Core.v b/theories/Categories/FunctorCategory/Core.v index 6a1323eb68e..20ea1fd9f53 100644 --- a/theories/Categories/FunctorCategory/Core.v +++ b/theories/Categories/FunctorCategory/Core.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. (** ** Definition of [C → D] *) Section functor_category. diff --git a/theories/Categories/FunctorCategory/Dual.v b/theories/Categories/FunctorCategory/Dual.v index 06db58b564b..5012aa160be 100644 --- a/theories/Categories/FunctorCategory/Dual.v +++ b/theories/Categories/FunctorCategory/Dual.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/FunctorCategory/Functorial.v b/theories/Categories/FunctorCategory/Functorial.v index 101d3feac97..fbfc62be7f0 100644 --- a/theories/Categories/FunctorCategory/Functorial.v +++ b/theories/Categories/FunctorCategory/Functorial.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope type_scope. diff --git a/theories/Categories/FunctorCategory/Morphisms.v b/theories/Categories/FunctorCategory/Morphisms.v index 7bd881d1e07..467ba2f449f 100644 --- a/theories/Categories/FunctorCategory/Morphisms.v +++ b/theories/Categories/FunctorCategory/Morphisms.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope category_scope. diff --git a/theories/Categories/FundamentalPreGroupoidCategory.v b/theories/Categories/FundamentalPreGroupoidCategory.v index dca017d67cc..a14f609383e 100644 --- a/theories/Categories/FundamentalPreGroupoidCategory.v +++ b/theories/Categories/FundamentalPreGroupoidCategory.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. diff --git a/theories/Categories/Grothendieck/PseudofunctorToCat.v b/theories/Categories/Grothendieck/PseudofunctorToCat.v index 6271de4c7a0..a253ab12cb5 100644 --- a/theories/Categories/Grothendieck/PseudofunctorToCat.v +++ b/theories/Categories/Grothendieck/PseudofunctorToCat.v @@ -12,7 +12,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Grothendieck/ToCat.v b/theories/Categories/Grothendieck/ToCat.v index 3de754da3f5..dc968e25e6c 100644 --- a/theories/Categories/Grothendieck/ToCat.v +++ b/theories/Categories/Grothendieck/ToCat.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Grothendieck/ToSet/Core.v b/theories/Categories/Grothendieck/ToSet/Core.v index dc348291dd6..da847c19e68 100644 --- a/theories/Categories/Grothendieck/ToSet/Core.v +++ b/theories/Categories/Grothendieck/ToSet/Core.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Grothendieck/ToSet/Morphisms.v b/theories/Categories/Grothendieck/ToSet/Morphisms.v index 33b0b16bb94..2fb6acfac52 100644 --- a/theories/Categories/Grothendieck/ToSet/Morphisms.v +++ b/theories/Categories/Grothendieck/ToSet/Morphisms.v @@ -9,7 +9,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Grothendieck/ToSet/Univalent.v b/theories/Categories/Grothendieck/ToSet/Univalent.v index 17b69ccd212..f4d31d39e5b 100644 --- a/theories/Categories/Grothendieck/ToSet/Univalent.v +++ b/theories/Categories/Grothendieck/ToSet/Univalent.v @@ -11,7 +11,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/GroupoidCategory/Core.v b/theories/Categories/GroupoidCategory/Core.v index fecf5d1f02c..15de726da77 100644 --- a/theories/Categories/GroupoidCategory/Core.v +++ b/theories/Categories/GroupoidCategory/Core.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/GroupoidCategory/Dual.v b/theories/Categories/GroupoidCategory/Dual.v index b4a63070cc4..0bdb572fcb1 100644 --- a/theories/Categories/GroupoidCategory/Dual.v +++ b/theories/Categories/GroupoidCategory/Dual.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/GroupoidCategory/Morphisms.v b/theories/Categories/GroupoidCategory/Morphisms.v index 140897b4199..a51b229b9ec 100644 --- a/theories/Categories/GroupoidCategory/Morphisms.v +++ b/theories/Categories/GroupoidCategory/Morphisms.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/HomFunctor.v b/theories/Categories/HomFunctor.v index 2d3cec9f9b6..481ab6823b6 100644 --- a/theories/Categories/HomFunctor.v +++ b/theories/Categories/HomFunctor.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/HomotopyPreCategory.v b/theories/Categories/HomotopyPreCategory.v index 05a9df0711e..07c2a69f709 100644 --- a/theories/Categories/HomotopyPreCategory.v +++ b/theories/Categories/HomotopyPreCategory.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. diff --git a/theories/Categories/IndiscreteCategory.v b/theories/Categories/IndiscreteCategory.v index 703a80b9406..a2245e9bec4 100644 --- a/theories/Categories/IndiscreteCategory.v +++ b/theories/Categories/IndiscreteCategory.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. (** ** Definition of an indiscrete category *) Module Export Core. diff --git a/theories/Categories/InitialTerminalCategory/Core.v b/theories/Categories/InitialTerminalCategory/Core.v index 23e90219815..50772ebafa3 100644 --- a/theories/Categories/InitialTerminalCategory/Core.v +++ b/theories/Categories/InitialTerminalCategory/Core.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Unset Primitive Projections. (* suppress a warning about [IsTerminalCategory] *) Notation initial_category := (nat_category 0) (only parsing). diff --git a/theories/Categories/InitialTerminalCategory/Functors.v b/theories/Categories/InitialTerminalCategory/Functors.v index 65cb971989e..95b8b5ce0d0 100644 --- a/theories/Categories/InitialTerminalCategory/Functors.v +++ b/theories/Categories/InitialTerminalCategory/Functors.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Section functors. Variable C : PreCategory. diff --git a/theories/Categories/InitialTerminalCategory/NaturalTransformations.v b/theories/Categories/InitialTerminalCategory/NaturalTransformations.v index 35b518d3900..0a5b8dc8059 100644 --- a/theories/Categories/InitialTerminalCategory/NaturalTransformations.v +++ b/theories/Categories/InitialTerminalCategory/NaturalTransformations.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Section NaturalTransformations. Variable C : PreCategory. diff --git a/theories/Categories/InitialTerminalCategory/Pseudofunctors.v b/theories/Categories/InitialTerminalCategory/Pseudofunctors.v index 0f03a3c6dc3..79909d25c54 100644 --- a/theories/Categories/InitialTerminalCategory/Pseudofunctors.v +++ b/theories/Categories/InitialTerminalCategory/Pseudofunctors.v @@ -12,7 +12,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Section pseudofunctors. (** ** Constant functor from any terminal category *) diff --git a/theories/Categories/KanExtensions/Core.v b/theories/Categories/KanExtensions/Core.v index fe0805bf057..b8d48f3f8e4 100644 --- a/theories/Categories/KanExtensions/Core.v +++ b/theories/Categories/KanExtensions/Core.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/KanExtensions/Functors.v b/theories/Categories/KanExtensions/Functors.v index b72623b086a..34a2b30da10 100644 --- a/theories/Categories/KanExtensions/Functors.v +++ b/theories/Categories/KanExtensions/Functors.v @@ -9,7 +9,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Section kan_extension_functors. Context `{Funext}. diff --git a/theories/Categories/LaxComma/Core.v b/theories/Categories/LaxComma/Core.v index ec9f5d744aa..b2f96c53647 100644 --- a/theories/Categories/LaxComma/Core.v +++ b/theories/Categories/LaxComma/Core.v @@ -17,7 +17,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/LaxComma/CoreLaws.v b/theories/Categories/LaxComma/CoreLaws.v index 30ba217a0bc..915d7bf5d1d 100644 --- a/theories/Categories/LaxComma/CoreLaws.v +++ b/theories/Categories/LaxComma/CoreLaws.v @@ -15,7 +15,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/LaxComma/CoreParts.v b/theories/Categories/LaxComma/CoreParts.v index e4009ebd26b..e59f1168e34 100644 --- a/theories/Categories/LaxComma/CoreParts.v +++ b/theories/Categories/LaxComma/CoreParts.v @@ -13,7 +13,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Limits/Core.v b/theories/Categories/Limits/Core.v index aa65452075a..d9c9368904f 100644 --- a/theories/Categories/Limits/Core.v +++ b/theories/Categories/Limits/Core.v @@ -12,7 +12,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/Limits/Functors.v b/theories/Categories/Limits/Functors.v index 8090e7dd3c8..d413f275c2b 100644 --- a/theories/Categories/Limits/Functors.v +++ b/theories/Categories/Limits/Functors.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. (** (co)limits assemble into functors *) diff --git a/theories/Categories/Monoidal/MonoidalCategory.v b/theories/Categories/Monoidal/MonoidalCategory.v index 174929eaefe..65172ed899e 100644 --- a/theories/Categories/Monoidal/MonoidalCategory.v +++ b/theories/Categories/Monoidal/MonoidalCategory.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Section MonoidalStructure. Context `{Funext}. diff --git a/theories/Categories/NatCategory.v b/theories/Categories/NatCategory.v index 898d31803a7..1641c1ea498 100644 --- a/theories/Categories/NatCategory.v +++ b/theories/Categories/NatCategory.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope nat_scope. Module Export Core. diff --git a/theories/Categories/NaturalTransformation/Composition/Core.v b/theories/Categories/NaturalTransformation/Composition/Core.v index 48f1dccd416..4ded6cd1254 100644 --- a/theories/Categories/NaturalTransformation/Composition/Core.v +++ b/theories/Categories/NaturalTransformation/Composition/Core.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/NaturalTransformation/Composition/Functorial.v b/theories/Categories/NaturalTransformation/Composition/Functorial.v index 6bd38ec72ca..d98b890c604 100644 --- a/theories/Categories/NaturalTransformation/Composition/Functorial.v +++ b/theories/Categories/NaturalTransformation/Composition/Functorial.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. diff --git a/theories/Categories/NaturalTransformation/Composition/Laws.v b/theories/Categories/NaturalTransformation/Composition/Laws.v index c04345f513a..f3122d48284 100644 --- a/theories/Categories/NaturalTransformation/Composition/Laws.v +++ b/theories/Categories/NaturalTransformation/Composition/Laws.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/NaturalTransformation/Core.v b/theories/Categories/NaturalTransformation/Core.v index 1929f5da485..c4234306d1f 100644 --- a/theories/Categories/NaturalTransformation/Core.v +++ b/theories/Categories/NaturalTransformation/Core.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Declare Scope natural_transformation_scope. Delimit Scope natural_transformation_scope with natural_transformation. diff --git a/theories/Categories/NaturalTransformation/Dual.v b/theories/Categories/NaturalTransformation/Dual.v index 9962737565b..40a50d88ed9 100644 --- a/theories/Categories/NaturalTransformation/Dual.v +++ b/theories/Categories/NaturalTransformation/Dual.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/NaturalTransformation/Identity.v b/theories/Categories/NaturalTransformation/Identity.v index 9917869a743..deaefb7dc03 100644 --- a/theories/Categories/NaturalTransformation/Identity.v +++ b/theories/Categories/NaturalTransformation/Identity.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope path_scope. diff --git a/theories/Categories/NaturalTransformation/Isomorphisms.v b/theories/Categories/NaturalTransformation/Isomorphisms.v index d870399a9dd..917b400b931 100644 --- a/theories/Categories/NaturalTransformation/Isomorphisms.v +++ b/theories/Categories/NaturalTransformation/Isomorphisms.v @@ -11,7 +11,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/NaturalTransformation/Paths.v b/theories/Categories/NaturalTransformation/Paths.v index 7a305abc381..f36dcfe7e9f 100644 --- a/theories/Categories/NaturalTransformation/Paths.v +++ b/theories/Categories/NaturalTransformation/Paths.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/NaturalTransformation/Pointwise.v b/theories/Categories/NaturalTransformation/Pointwise.v index 5531e9aea3b..9a3532cd01d 100644 --- a/theories/Categories/NaturalTransformation/Pointwise.v +++ b/theories/Categories/NaturalTransformation/Pointwise.v @@ -7,7 +7,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. (** Recall that a "pointwise" functor is a functor [Aᴮ → Cᴰ] induced by functors [D → B] and [A → C]. Given two functors [D → B] and a diff --git a/theories/Categories/NaturalTransformation/Prod.v b/theories/Categories/NaturalTransformation/Prod.v index 52c5551040a..4d6c887a6e4 100644 --- a/theories/Categories/NaturalTransformation/Prod.v +++ b/theories/Categories/NaturalTransformation/Prod.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. (** ** Product of natural transformations *) Section prod. diff --git a/theories/Categories/NaturalTransformation/Sum.v b/theories/Categories/NaturalTransformation/Sum.v index 50a79ddafe6..abbf1d7551b 100644 --- a/theories/Categories/NaturalTransformation/Sum.v +++ b/theories/Categories/NaturalTransformation/Sum.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Section sum. Definition sum diff --git a/theories/Categories/ProductLaws.v b/theories/Categories/ProductLaws.v index 75af90b6b3f..e1cfaaaa9a3 100644 --- a/theories/Categories/ProductLaws.v +++ b/theories/Categories/ProductLaws.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope functor_scope. diff --git a/theories/Categories/Profunctor/Core.v b/theories/Categories/Profunctor/Core.v index fb493307a23..bba649ba0f8 100644 --- a/theories/Categories/Profunctor/Core.v +++ b/theories/Categories/Profunctor/Core.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Declare Scope profunctor_scope. Delimit Scope profunctor_scope with profunctor. diff --git a/theories/Categories/Profunctor/Identity.v b/theories/Categories/Profunctor/Identity.v index 714c75667ea..1cbe9ee911e 100644 --- a/theories/Categories/Profunctor/Identity.v +++ b/theories/Categories/Profunctor/Identity.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope profunctor_scope. diff --git a/theories/Categories/Profunctor/Representable.v b/theories/Categories/Profunctor/Representable.v index 82c0c7d095a..e0aa656cff0 100644 --- a/theories/Categories/Profunctor/Representable.v +++ b/theories/Categories/Profunctor/Representable.v @@ -5,7 +5,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. Local Open Scope profunctor_scope. diff --git a/theories/Categories/Pseudofunctor/Core.v b/theories/Categories/Pseudofunctor/Core.v index 77e35624dda..367f3f06168 100644 --- a/theories/Categories/Pseudofunctor/Core.v +++ b/theories/Categories/Pseudofunctor/Core.v @@ -9,7 +9,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Pseudofunctor/FromFunctor.v b/theories/Categories/Pseudofunctor/FromFunctor.v index afb1773708e..42fc9830f7e 100644 --- a/theories/Categories/Pseudofunctor/FromFunctor.v +++ b/theories/Categories/Pseudofunctor/FromFunctor.v @@ -13,7 +13,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Pseudofunctor/Identity.v b/theories/Categories/Pseudofunctor/Identity.v index 822cc32b85c..ed9548e45f5 100644 --- a/theories/Categories/Pseudofunctor/Identity.v +++ b/theories/Categories/Pseudofunctor/Identity.v @@ -18,7 +18,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope natural_transformation_scope. diff --git a/theories/Categories/Pseudofunctor/RewriteLaws.v b/theories/Categories/Pseudofunctor/RewriteLaws.v index 020cf9c36c1..ad90fa93591 100644 --- a/theories/Categories/Pseudofunctor/RewriteLaws.v +++ b/theories/Categories/Pseudofunctor/RewriteLaws.v @@ -13,7 +13,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/PseudonaturalTransformation/Core.v b/theories/Categories/PseudonaturalTransformation/Core.v index 666f7d50c94..fab8a91a0cd 100644 --- a/theories/Categories/PseudonaturalTransformation/Core.v +++ b/theories/Categories/PseudonaturalTransformation/Core.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Declare Scope pseudonatural_transformation_scope. Delimit Scope pseudonatural_transformation_scope with pseudonatural_transformation. diff --git a/theories/Categories/SemiSimplicialSets.v b/theories/Categories/SemiSimplicialSets.v index d65222cb034..ac51d13090b 100644 --- a/theories/Categories/SemiSimplicialSets.v +++ b/theories/Categories/SemiSimplicialSets.v @@ -11,7 +11,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. diff --git a/theories/Categories/SetCategory/Core.v b/theories/Categories/SetCategory/Core.v index 862394655c8..274b1f3bcbd 100644 --- a/theories/Categories/SetCategory/Core.v +++ b/theories/Categories/SetCategory/Core.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Notation cat_of obj := (@Build_PreCategory obj diff --git a/theories/Categories/SetCategory/Functors/SetProp.v b/theories/Categories/SetCategory/Functors/SetProp.v index cdf46c60981..c9dc9127d91 100644 --- a/theories/Categories/SetCategory/Functors/SetProp.v +++ b/theories/Categories/SetCategory/Functors/SetProp.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Section set_coercions_definitions. Context `{Funext}. diff --git a/theories/Categories/SetCategory/Morphisms.v b/theories/Categories/SetCategory/Morphisms.v index d6cef2227a3..8b5221a1d93 100644 --- a/theories/Categories/SetCategory/Morphisms.v +++ b/theories/Categories/SetCategory/Morphisms.v @@ -9,7 +9,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. diff --git a/theories/Categories/SimplicialSets.v b/theories/Categories/SimplicialSets.v index edd1cc49390..e1a29f427aa 100644 --- a/theories/Categories/SimplicialSets.v +++ b/theories/Categories/SimplicialSets.v @@ -10,7 +10,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope functor_scope. Local Open Scope category_scope. diff --git a/theories/Categories/Structure/Core.v b/theories/Categories/Structure/Core.v index ad0994abc62..7a4f416e687 100644 --- a/theories/Categories/Structure/Core.v +++ b/theories/Categories/Structure/Core.v @@ -6,7 +6,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope category_scope. Local Open Scope morphism_scope. diff --git a/theories/Categories/Structure/IdentityPrinciple.v b/theories/Categories/Structure/IdentityPrinciple.v index 915df617623..ab149e36cb5 100644 --- a/theories/Categories/Structure/IdentityPrinciple.v +++ b/theories/Categories/Structure/IdentityPrinciple.v @@ -8,7 +8,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope path_scope. Local Open Scope category_scope. diff --git a/theories/Categories/UniversalProperties.v b/theories/Categories/UniversalProperties.v index 6c2d68aac60..e2094a36fc5 100644 --- a/theories/Categories/UniversalProperties.v +++ b/theories/Categories/UniversalProperties.v @@ -14,7 +14,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. diff --git a/theories/Categories/Yoneda.v b/theories/Categories/Yoneda.v index 7709b99fed3..129a85c8e3c 100644 --- a/theories/Categories/Yoneda.v +++ b/theories/Categories/Yoneda.v @@ -16,7 +16,8 @@ Set Universe Polymorphism. Set Implicit Arguments. Generalizable All Variables. Set Asymmetric Patterns. -#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits. +#[warning="-unknown-option"] +Set Asymmetric Patterns No Implicits. Local Open Scope morphism_scope. Local Open Scope category_scope.