From 9d1829649c26c4b1607635314d2a4c822aed6805 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 24 Apr 2026 17:54:51 +0000
Subject: [PATCH] Style: put asymmetric patterns commands on separate lines

Split the combined `Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.` line into separate lines across all 127 affected files:

    Set Asymmetric Patterns.
    #[warning="-unknown-option"]
    Set Asymmetric Patterns No Implicits.

Also add a comment in `theories/Basics/Settings.v` noting that the
warning clause can be removed once our minimum Rocq version is 9.3.

Agent-Logs-Url: https://github.com/HoTT/Coq-HoTT/sessions/cf924724-049b-4592-8215-90cea9e6fef7

Co-authored-by: Alizter <8614547+Alizter@users.noreply.github.com>
---
 theories/Basics/Settings.v                                   | 5 ++++-
 theories/Categories/Adjoint/Composition/AssociativityLaw.v   | 4 +++-
 theories/Categories/Adjoint/Composition/Core.v               | 4 +++-
 theories/Categories/Adjoint/Composition/IdentityLaws.v       | 4 +++-
 theories/Categories/Adjoint/Composition/LawsTactic.v         | 4 +++-
 theories/Categories/Adjoint/Dual.v                           | 4 +++-
 theories/Categories/Adjoint/Functorial/Core.v                | 4 +++-
 theories/Categories/Adjoint/Functorial/Laws.v                | 4 +++-
 theories/Categories/Adjoint/Functorial/Parts.v               | 4 +++-
 theories/Categories/Adjoint/Hom.v                            | 4 +++-
 theories/Categories/Adjoint/HomCoercions.v                   | 4 +++-
 theories/Categories/Adjoint/Identity.v                       | 4 +++-
 theories/Categories/Adjoint/Paths.v                          | 4 +++-
 theories/Categories/Adjoint/Pointwise.v                      | 4 +++-
 theories/Categories/Adjoint/UnitCounit.v                     | 4 +++-
 theories/Categories/Adjoint/UnitCounitCoercions.v            | 4 +++-
 theories/Categories/Adjoint/UniversalMorphisms/Core.v        | 4 +++-
 theories/Categories/Cat/Core.v                               | 4 +++-
 theories/Categories/Cat/Morphisms.v                          | 4 +++-
 theories/Categories/Category/Core.v                          | 4 +++-
 theories/Categories/Category/Dual.v                          | 4 +++-
 theories/Categories/Category/Morphisms.v                     | 4 +++-
 theories/Categories/Category/Objects.v                       | 4 +++-
 theories/Categories/Category/Paths.v                         | 4 +++-
 theories/Categories/Category/Pi.v                            | 4 +++-
 theories/Categories/Category/Prod.v                          | 4 +++-
 theories/Categories/Category/Sigma/Core.v                    | 4 +++-
 theories/Categories/Category/Sigma/OnMorphisms.v             | 4 +++-
 theories/Categories/Category/Sigma/OnObjects.v               | 4 +++-
 theories/Categories/Category/Sigma/Univalent.v               | 4 +++-
 theories/Categories/Category/Strict.v                        | 4 +++-
 theories/Categories/Category/Sum.v                           | 4 +++-
 theories/Categories/Category/Univalent.v                     | 4 +++-
 theories/Categories/CategoryOfGroupoids.v                    | 4 +++-
 theories/Categories/CategoryOfSections/Core.v                | 4 +++-
 theories/Categories/ChainCategory.v                          | 4 +++-
 theories/Categories/Comma/Core.v                             | 4 +++-
 theories/Categories/Comma/Dual.v                             | 4 +++-
 theories/Categories/Comma/Functorial.v                       | 4 +++-
 theories/Categories/Comma/InducedFunctors.v                  | 4 +++-
 theories/Categories/Comma/Projection.v                       | 4 +++-
 theories/Categories/Comma/ProjectionFunctors.v               | 4 +++-
 theories/Categories/DependentProduct.v                       | 4 +++-
 theories/Categories/DiscreteCategory.v                       | 4 +++-
 theories/Categories/DualFunctor.v                            | 4 +++-
 theories/Categories/ExponentialLaws/Law0.v                   | 4 +++-
 theories/Categories/ExponentialLaws/Law1/Functors.v          | 4 +++-
 theories/Categories/ExponentialLaws/Law1/Law.v               | 4 +++-
 theories/Categories/ExponentialLaws/Law2/Functors.v          | 4 +++-
 theories/Categories/ExponentialLaws/Law2/Law.v               | 4 +++-
 theories/Categories/ExponentialLaws/Law3/Functors.v          | 4 +++-
 theories/Categories/ExponentialLaws/Law3/Law.v               | 4 +++-
 theories/Categories/ExponentialLaws/Law4/Functors.v          | 4 +++-
 theories/Categories/ExponentialLaws/Law4/Law.v               | 4 +++-
 theories/Categories/Functor/Attributes.v                     | 4 +++-
 theories/Categories/Functor/Composition/Core.v               | 4 +++-
 .../Categories/Functor/Composition/Functorial/Attributes.v   | 4 +++-
 theories/Categories/Functor/Composition/Functorial/Core.v    | 4 +++-
 theories/Categories/Functor/Composition/Laws.v               | 4 +++-
 theories/Categories/Functor/Core.v                           | 4 +++-
 theories/Categories/Functor/Dual.v                           | 4 +++-
 theories/Categories/Functor/Identity.v                       | 4 +++-
 theories/Categories/Functor/Paths.v                          | 4 +++-
 theories/Categories/Functor/Pointwise/Core.v                 | 4 +++-
 theories/Categories/Functor/Pointwise/Properties.v           | 4 +++-
 theories/Categories/Functor/Prod/Core.v                      | 4 +++-
 theories/Categories/Functor/Prod/Functorial.v                | 4 +++-
 theories/Categories/Functor/Prod/Universal.v                 | 4 +++-
 theories/Categories/Functor/Sum.v                            | 4 +++-
 theories/Categories/FunctorCategory/Core.v                   | 4 +++-
 theories/Categories/FunctorCategory/Dual.v                   | 4 +++-
 theories/Categories/FunctorCategory/Functorial.v             | 4 +++-
 theories/Categories/FunctorCategory/Morphisms.v              | 4 +++-
 theories/Categories/FundamentalPreGroupoidCategory.v         | 4 +++-
 theories/Categories/Grothendieck/PseudofunctorToCat.v        | 4 +++-
 theories/Categories/Grothendieck/ToCat.v                     | 4 +++-
 theories/Categories/Grothendieck/ToSet/Core.v                | 4 +++-
 theories/Categories/Grothendieck/ToSet/Morphisms.v           | 4 +++-
 theories/Categories/Grothendieck/ToSet/Univalent.v           | 4 +++-
 theories/Categories/GroupoidCategory/Core.v                  | 4 +++-
 theories/Categories/GroupoidCategory/Dual.v                  | 4 +++-
 theories/Categories/GroupoidCategory/Morphisms.v             | 4 +++-
 theories/Categories/HomFunctor.v                             | 4 +++-
 theories/Categories/HomotopyPreCategory.v                    | 4 +++-
 theories/Categories/IndiscreteCategory.v                     | 4 +++-
 theories/Categories/InitialTerminalCategory/Core.v           | 4 +++-
 theories/Categories/InitialTerminalCategory/Functors.v       | 4 +++-
 .../InitialTerminalCategory/NaturalTransformations.v         | 4 +++-
 theories/Categories/InitialTerminalCategory/Pseudofunctors.v | 4 +++-
 theories/Categories/KanExtensions/Core.v                     | 4 +++-
 theories/Categories/KanExtensions/Functors.v                 | 4 +++-
 theories/Categories/LaxComma/Core.v                          | 4 +++-
 theories/Categories/LaxComma/CoreLaws.v                      | 4 +++-
 theories/Categories/LaxComma/CoreParts.v                     | 4 +++-
 theories/Categories/Limits/Core.v                            | 4 +++-
 theories/Categories/Limits/Functors.v                        | 4 +++-
 theories/Categories/Monoidal/MonoidalCategory.v              | 4 +++-
 theories/Categories/NatCategory.v                            | 4 +++-
 theories/Categories/NaturalTransformation/Composition/Core.v | 4 +++-
 .../NaturalTransformation/Composition/Functorial.v           | 4 +++-
 theories/Categories/NaturalTransformation/Composition/Laws.v | 4 +++-
 theories/Categories/NaturalTransformation/Core.v             | 4 +++-
 theories/Categories/NaturalTransformation/Dual.v             | 4 +++-
 theories/Categories/NaturalTransformation/Identity.v         | 4 +++-
 theories/Categories/NaturalTransformation/Isomorphisms.v     | 4 +++-
 theories/Categories/NaturalTransformation/Paths.v            | 4 +++-
 theories/Categories/NaturalTransformation/Pointwise.v        | 4 +++-
 theories/Categories/NaturalTransformation/Prod.v             | 4 +++-
 theories/Categories/NaturalTransformation/Sum.v              | 4 +++-
 theories/Categories/ProductLaws.v                            | 4 +++-
 theories/Categories/Profunctor/Core.v                        | 4 +++-
 theories/Categories/Profunctor/Identity.v                    | 4 +++-
 theories/Categories/Profunctor/Representable.v               | 4 +++-
 theories/Categories/Pseudofunctor/Core.v                     | 4 +++-
 theories/Categories/Pseudofunctor/FromFunctor.v              | 4 +++-
 theories/Categories/Pseudofunctor/Identity.v                 | 4 +++-
 theories/Categories/Pseudofunctor/RewriteLaws.v              | 4 +++-
 theories/Categories/PseudonaturalTransformation/Core.v       | 4 +++-
 theories/Categories/SemiSimplicialSets.v                     | 4 +++-
 theories/Categories/SetCategory/Core.v                       | 4 +++-
 theories/Categories/SetCategory/Functors/SetProp.v           | 4 +++-
 theories/Categories/SetCategory/Morphisms.v                  | 4 +++-
 theories/Categories/SimplicialSets.v                         | 4 +++-
 theories/Categories/Structure/Core.v                         | 4 +++-
 theories/Categories/Structure/IdentityPrinciple.v            | 4 +++-
 theories/Categories/UniversalProperties.v                    | 4 +++-
 theories/Categories/Yoneda.v                                 | 4 +++-
 127 files changed, 382 insertions(+), 127 deletions(-)

diff --git a/theories/Basics/Settings.v b/theories/Basics/Settings.v
index 46d7594ebd9..2f895e2effd 100644
--- a/theories/Basics/Settings.v
+++ b/theories/Basics/Settings.v
@@ -42,7 +42,10 @@ 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.
+(** 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 ffaa80735c4..decac5e8a85 100644
--- a/theories/Categories/Adjoint/Composition/AssociativityLaw.v
+++ b/theories/Categories/Adjoint/Composition/AssociativityLaw.v
@@ -7,7 +7,9 @@ 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..7e4f0ed75b2 100644
--- a/theories/Categories/Adjoint/Composition/Core.v
+++ b/theories/Categories/Adjoint/Composition/Core.v
@@ -10,7 +10,9 @@ 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..bab836b0010 100644
--- a/theories/Categories/Adjoint/Composition/IdentityLaws.v
+++ b/theories/Categories/Adjoint/Composition/IdentityLaws.v
@@ -7,7 +7,9 @@ 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..c6c3cdcb96e 100644
--- a/theories/Categories/Adjoint/Composition/LawsTactic.v
+++ b/theories/Categories/Adjoint/Composition/LawsTactic.v
@@ -7,7 +7,9 @@ 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..99af2b42fff 100644
--- a/theories/Categories/Adjoint/Dual.v
+++ b/theories/Categories/Adjoint/Dual.v
@@ -6,7 +6,9 @@ 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..b6722981210 100644
--- a/theories/Categories/Adjoint/Functorial/Core.v
+++ b/theories/Categories/Adjoint/Functorial/Core.v
@@ -10,7 +10,9 @@ 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..d22f5187a17 100644
--- a/theories/Categories/Adjoint/Functorial/Laws.v
+++ b/theories/Categories/Adjoint/Functorial/Laws.v
@@ -13,7 +13,9 @@ 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..abfb7fd8243 100644
--- a/theories/Categories/Adjoint/Functorial/Parts.v
+++ b/theories/Categories/Adjoint/Functorial/Parts.v
@@ -8,7 +8,9 @@ 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..dbce1b3aa13 100644
--- a/theories/Categories/Adjoint/Hom.v
+++ b/theories/Categories/Adjoint/Hom.v
@@ -11,7 +11,9 @@ 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..dea732fdf69 100644
--- a/theories/Categories/Adjoint/HomCoercions.v
+++ b/theories/Categories/Adjoint/HomCoercions.v
@@ -11,7 +11,9 @@ 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..355206469ad 100644
--- a/theories/Categories/Adjoint/Identity.v
+++ b/theories/Categories/Adjoint/Identity.v
@@ -6,7 +6,9 @@ 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..318415ebe18 100644
--- a/theories/Categories/Adjoint/Paths.v
+++ b/theories/Categories/Adjoint/Paths.v
@@ -8,7 +8,9 @@ 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..21dc6f4d953 100644
--- a/theories/Categories/Adjoint/Pointwise.v
+++ b/theories/Categories/Adjoint/Pointwise.v
@@ -15,7 +15,9 @@ 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..1172991cd6e 100644
--- a/theories/Categories/Adjoint/UnitCounit.v
+++ b/theories/Categories/Adjoint/UnitCounit.v
@@ -6,7 +6,9 @@ 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..a47f42999fa 100644
--- a/theories/Categories/Adjoint/UnitCounitCoercions.v
+++ b/theories/Categories/Adjoint/UnitCounitCoercions.v
@@ -8,7 +8,9 @@ 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..224edbe875a 100644
--- a/theories/Categories/Adjoint/UniversalMorphisms/Core.v
+++ b/theories/Categories/Adjoint/UniversalMorphisms/Core.v
@@ -12,7 +12,9 @@ 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..a4a2a4e29b6 100644
--- a/theories/Categories/Cat/Core.v
+++ b/theories/Categories/Cat/Core.v
@@ -5,7 +5,9 @@ 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..fb6996a22a9 100644
--- a/theories/Categories/Cat/Morphisms.v
+++ b/theories/Categories/Cat/Morphisms.v
@@ -5,7 +5,9 @@ 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..4b413b22c41 100644
--- a/theories/Categories/Category/Core.v
+++ b/theories/Categories/Category/Core.v
@@ -4,7 +4,9 @@ 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..8ef3725ff94 100644
--- a/theories/Categories/Category/Dual.v
+++ b/theories/Categories/Category/Dual.v
@@ -4,7 +4,9 @@ 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..a0f00952ab1 100644
--- a/theories/Categories/Category/Morphisms.v
+++ b/theories/Categories/Category/Morphisms.v
@@ -5,7 +5,9 @@ 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..abc72a5e7ba 100644
--- a/theories/Categories/Category/Objects.v
+++ b/theories/Categories/Category/Objects.v
@@ -5,7 +5,9 @@ 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..a89c19d7eab 100644
--- a/theories/Categories/Category/Paths.v
+++ b/theories/Categories/Category/Paths.v
@@ -7,7 +7,9 @@ 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..780220926cd 100644
--- a/theories/Categories/Category/Pi.v
+++ b/theories/Categories/Category/Pi.v
@@ -5,7 +5,9 @@ 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..c8ba0658dd7 100644
--- a/theories/Categories/Category/Prod.v
+++ b/theories/Categories/Category/Prod.v
@@ -6,7 +6,9 @@ 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..74bb1cb7a27 100644
--- a/theories/Categories/Category/Sigma/Core.v
+++ b/theories/Categories/Category/Sigma/Core.v
@@ -5,7 +5,9 @@ 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..835f1e67f45 100644
--- a/theories/Categories/Category/Sigma/OnMorphisms.v
+++ b/theories/Categories/Category/Sigma/OnMorphisms.v
@@ -9,7 +9,9 @@ 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..848de599672 100644
--- a/theories/Categories/Category/Sigma/OnObjects.v
+++ b/theories/Categories/Category/Sigma/OnObjects.v
@@ -9,7 +9,9 @@ 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..4412f6fb699 100644
--- a/theories/Categories/Category/Sigma/Univalent.v
+++ b/theories/Categories/Category/Sigma/Univalent.v
@@ -7,7 +7,9 @@ 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..ef85361e797 100644
--- a/theories/Categories/Category/Strict.v
+++ b/theories/Categories/Category/Strict.v
@@ -4,7 +4,9 @@ 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..9de227d5f41 100644
--- a/theories/Categories/Category/Sum.v
+++ b/theories/Categories/Category/Sum.v
@@ -4,7 +4,9 @@ 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..950b0b6e22b 100644
--- a/theories/Categories/Category/Univalent.v
+++ b/theories/Categories/Category/Univalent.v
@@ -5,7 +5,9 @@ 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..e66131d6c81 100644
--- a/theories/Categories/CategoryOfGroupoids.v
+++ b/theories/Categories/CategoryOfGroupoids.v
@@ -7,7 +7,9 @@ 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..1e607d3b070 100644
--- a/theories/Categories/CategoryOfSections/Core.v
+++ b/theories/Categories/CategoryOfSections/Core.v
@@ -9,7 +9,9 @@ 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..9642c0826af 100644
--- a/theories/Categories/ChainCategory.v
+++ b/theories/Categories/ChainCategory.v
@@ -7,7 +7,9 @@ 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..1e5f6681dd9 100644
--- a/theories/Categories/Comma/Core.v
+++ b/theories/Categories/Comma/Core.v
@@ -9,7 +9,9 @@ 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..bad79776e4f 100644
--- a/theories/Categories/Comma/Dual.v
+++ b/theories/Categories/Comma/Dual.v
@@ -10,7 +10,9 @@ 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..4a77516040f 100644
--- a/theories/Categories/Comma/Functorial.v
+++ b/theories/Categories/Comma/Functorial.v
@@ -14,7 +14,9 @@ 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..5441d1cec5e 100644
--- a/theories/Categories/Comma/InducedFunctors.v
+++ b/theories/Categories/Comma/InducedFunctors.v
@@ -15,7 +15,9 @@ 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..78f97655e5b 100644
--- a/theories/Categories/Comma/Projection.v
+++ b/theories/Categories/Comma/Projection.v
@@ -12,7 +12,9 @@ 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..271590f400f 100644
--- a/theories/Categories/Comma/ProjectionFunctors.v
+++ b/theories/Categories/Comma/ProjectionFunctors.v
@@ -18,7 +18,9 @@ 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..a6e3d856ec1 100644
--- a/theories/Categories/DependentProduct.v
+++ b/theories/Categories/DependentProduct.v
@@ -7,7 +7,9 @@ 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..2e10a6ae9e7 100644
--- a/theories/Categories/DiscreteCategory.v
+++ b/theories/Categories/DiscreteCategory.v
@@ -4,7 +4,9 @@ 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..7f9775422a6 100644
--- a/theories/Categories/DualFunctor.v
+++ b/theories/Categories/DualFunctor.v
@@ -8,7 +8,9 @@ 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..1dfe7f33c5e 100644
--- a/theories/Categories/ExponentialLaws/Law0.v
+++ b/theories/Categories/ExponentialLaws/Law0.v
@@ -6,7 +6,9 @@ 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..9e41b3e9208 100644
--- a/theories/Categories/ExponentialLaws/Law1/Functors.v
+++ b/theories/Categories/ExponentialLaws/Law1/Functors.v
@@ -6,7 +6,9 @@ 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..5e5193cf229 100644
--- a/theories/Categories/ExponentialLaws/Law1/Law.v
+++ b/theories/Categories/ExponentialLaws/Law1/Law.v
@@ -7,7 +7,9 @@ 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..b63b8e522d1 100644
--- a/theories/Categories/ExponentialLaws/Law2/Functors.v
+++ b/theories/Categories/ExponentialLaws/Law2/Functors.v
@@ -4,7 +4,9 @@ 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..484d6d8cac5 100644
--- a/theories/Categories/ExponentialLaws/Law2/Law.v
+++ b/theories/Categories/ExponentialLaws/Law2/Law.v
@@ -9,7 +9,9 @@ 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..fe8ef14e325 100644
--- a/theories/Categories/ExponentialLaws/Law3/Functors.v
+++ b/theories/Categories/ExponentialLaws/Law3/Functors.v
@@ -6,7 +6,9 @@ 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..bfa05262ca7 100644
--- a/theories/Categories/ExponentialLaws/Law3/Law.v
+++ b/theories/Categories/ExponentialLaws/Law3/Law.v
@@ -9,7 +9,9 @@ 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..14107106d7a 100644
--- a/theories/Categories/ExponentialLaws/Law4/Functors.v
+++ b/theories/Categories/ExponentialLaws/Law4/Functors.v
@@ -5,7 +5,9 @@ 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..0605ff9d19c 100644
--- a/theories/Categories/ExponentialLaws/Law4/Law.v
+++ b/theories/Categories/ExponentialLaws/Law4/Law.v
@@ -8,7 +8,9 @@ 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..b4a20ec10c3 100644
--- a/theories/Categories/Functor/Attributes.v
+++ b/theories/Categories/Functor/Attributes.v
@@ -5,7 +5,9 @@ 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..eab48b66699 100644
--- a/theories/Categories/Functor/Composition/Core.v
+++ b/theories/Categories/Functor/Composition/Core.v
@@ -4,7 +4,9 @@ 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..c9065145836 100644
--- a/theories/Categories/Functor/Composition/Functorial/Attributes.v
+++ b/theories/Categories/Functor/Composition/Functorial/Attributes.v
@@ -12,7 +12,9 @@ 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..62044d6dcd4 100644
--- a/theories/Categories/Functor/Composition/Functorial/Core.v
+++ b/theories/Categories/Functor/Composition/Functorial/Core.v
@@ -8,7 +8,9 @@ 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..addcff84a6e 100644
--- a/theories/Categories/Functor/Composition/Laws.v
+++ b/theories/Categories/Functor/Composition/Laws.v
@@ -6,7 +6,9 @@ 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..3662bb83bfa 100644
--- a/theories/Categories/Functor/Core.v
+++ b/theories/Categories/Functor/Core.v
@@ -4,7 +4,9 @@ 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..36676db4dd0 100644
--- a/theories/Categories/Functor/Dual.v
+++ b/theories/Categories/Functor/Dual.v
@@ -6,7 +6,9 @@ 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..9116d16f639 100644
--- a/theories/Categories/Functor/Identity.v
+++ b/theories/Categories/Functor/Identity.v
@@ -4,7 +4,9 @@ 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..79adb66b6a0 100644
--- a/theories/Categories/Functor/Paths.v
+++ b/theories/Categories/Functor/Paths.v
@@ -5,7 +5,9 @@ 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..d55c28d2feb 100644
--- a/theories/Categories/Functor/Pointwise/Core.v
+++ b/theories/Categories/Functor/Pointwise/Core.v
@@ -4,7 +4,9 @@ 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..0fcde0bc2ff 100644
--- a/theories/Categories/Functor/Pointwise/Properties.v
+++ b/theories/Categories/Functor/Pointwise/Properties.v
@@ -6,7 +6,9 @@ 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..4da1b230a7f 100644
--- a/theories/Categories/Functor/Prod/Core.v
+++ b/theories/Categories/Functor/Prod/Core.v
@@ -5,7 +5,9 @@ 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..45a8579cc06 100644
--- a/theories/Categories/Functor/Prod/Functorial.v
+++ b/theories/Categories/Functor/Prod/Functorial.v
@@ -5,7 +5,9 @@ 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..6beb025b088 100644
--- a/theories/Categories/Functor/Prod/Universal.v
+++ b/theories/Categories/Functor/Prod/Universal.v
@@ -7,7 +7,9 @@ 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..7d58a047517 100644
--- a/theories/Categories/Functor/Sum.v
+++ b/theories/Categories/Functor/Sum.v
@@ -6,7 +6,9 @@ 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..20ea1fd9f53 100644
--- a/theories/Categories/FunctorCategory/Core.v
+++ b/theories/Categories/FunctorCategory/Core.v
@@ -6,7 +6,9 @@ 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..5012aa160be 100644
--- a/theories/Categories/FunctorCategory/Dual.v
+++ b/theories/Categories/FunctorCategory/Dual.v
@@ -9,7 +9,9 @@ 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..fbfc62be7f0 100644
--- a/theories/Categories/FunctorCategory/Functorial.v
+++ b/theories/Categories/FunctorCategory/Functorial.v
@@ -4,7 +4,9 @@ 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..467ba2f449f 100644
--- a/theories/Categories/FunctorCategory/Morphisms.v
+++ b/theories/Categories/FunctorCategory/Morphisms.v
@@ -5,7 +5,9 @@ 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..a14f609383e 100644
--- a/theories/Categories/FundamentalPreGroupoidCategory.v
+++ b/theories/Categories/FundamentalPreGroupoidCategory.v
@@ -6,7 +6,9 @@ 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..a253ab12cb5 100644
--- a/theories/Categories/Grothendieck/PseudofunctorToCat.v
+++ b/theories/Categories/Grothendieck/PseudofunctorToCat.v
@@ -11,7 +11,9 @@ 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..dc968e25e6c 100644
--- a/theories/Categories/Grothendieck/ToCat.v
+++ b/theories/Categories/Grothendieck/ToCat.v
@@ -7,7 +7,9 @@ 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..da847c19e68 100644
--- a/theories/Categories/Grothendieck/ToSet/Core.v
+++ b/theories/Categories/Grothendieck/ToSet/Core.v
@@ -7,7 +7,9 @@ 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..2fb6acfac52 100644
--- a/theories/Categories/Grothendieck/ToSet/Morphisms.v
+++ b/theories/Categories/Grothendieck/ToSet/Morphisms.v
@@ -8,7 +8,9 @@ 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..f4d31d39e5b 100644
--- a/theories/Categories/Grothendieck/ToSet/Univalent.v
+++ b/theories/Categories/Grothendieck/ToSet/Univalent.v
@@ -10,7 +10,9 @@ 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..15de726da77 100644
--- a/theories/Categories/GroupoidCategory/Core.v
+++ b/theories/Categories/GroupoidCategory/Core.v
@@ -5,7 +5,9 @@ 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..0bdb572fcb1 100644
--- a/theories/Categories/GroupoidCategory/Dual.v
+++ b/theories/Categories/GroupoidCategory/Dual.v
@@ -6,7 +6,9 @@ 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..a51b229b9ec 100644
--- a/theories/Categories/GroupoidCategory/Morphisms.v
+++ b/theories/Categories/GroupoidCategory/Morphisms.v
@@ -5,7 +5,9 @@ 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..481ab6823b6 100644
--- a/theories/Categories/HomFunctor.v
+++ b/theories/Categories/HomFunctor.v
@@ -7,7 +7,9 @@ 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..07c2a69f709 100644
--- a/theories/Categories/HomotopyPreCategory.v
+++ b/theories/Categories/HomotopyPreCategory.v
@@ -5,7 +5,9 @@ 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..a2245e9bec4 100644
--- a/theories/Categories/IndiscreteCategory.v
+++ b/theories/Categories/IndiscreteCategory.v
@@ -5,7 +5,9 @@ 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..50772ebafa3 100644
--- a/theories/Categories/InitialTerminalCategory/Core.v
+++ b/theories/Categories/InitialTerminalCategory/Core.v
@@ -6,7 +6,9 @@ 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..95b8b5ce0d0 100644
--- a/theories/Categories/InitialTerminalCategory/Functors.v
+++ b/theories/Categories/InitialTerminalCategory/Functors.v
@@ -7,7 +7,9 @@ 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..0a5b8dc8059 100644
--- a/theories/Categories/InitialTerminalCategory/NaturalTransformations.v
+++ b/theories/Categories/InitialTerminalCategory/NaturalTransformations.v
@@ -6,7 +6,9 @@ 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..79909d25c54 100644
--- a/theories/Categories/InitialTerminalCategory/Pseudofunctors.v
+++ b/theories/Categories/InitialTerminalCategory/Pseudofunctors.v
@@ -11,7 +11,9 @@ 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..b8d48f3f8e4 100644
--- a/theories/Categories/KanExtensions/Core.v
+++ b/theories/Categories/KanExtensions/Core.v
@@ -7,7 +7,9 @@ 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..34a2b30da10 100644
--- a/theories/Categories/KanExtensions/Functors.v
+++ b/theories/Categories/KanExtensions/Functors.v
@@ -8,7 +8,9 @@ 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..b2f96c53647 100644
--- a/theories/Categories/LaxComma/Core.v
+++ b/theories/Categories/LaxComma/Core.v
@@ -16,7 +16,9 @@ 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..915d7bf5d1d 100644
--- a/theories/Categories/LaxComma/CoreLaws.v
+++ b/theories/Categories/LaxComma/CoreLaws.v
@@ -14,7 +14,9 @@ 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..e59f1168e34 100644
--- a/theories/Categories/LaxComma/CoreParts.v
+++ b/theories/Categories/LaxComma/CoreParts.v
@@ -12,7 +12,9 @@ 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..d9c9368904f 100644
--- a/theories/Categories/Limits/Core.v
+++ b/theories/Categories/Limits/Core.v
@@ -11,7 +11,9 @@ 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..d413f275c2b 100644
--- a/theories/Categories/Limits/Functors.v
+++ b/theories/Categories/Limits/Functors.v
@@ -9,7 +9,9 @@ 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..65172ed899e 100644
--- a/theories/Categories/Monoidal/MonoidalCategory.v
+++ b/theories/Categories/Monoidal/MonoidalCategory.v
@@ -9,7 +9,9 @@ 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..1641c1ea498 100644
--- a/theories/Categories/NatCategory.v
+++ b/theories/Categories/NatCategory.v
@@ -6,7 +6,9 @@ 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..4ded6cd1254 100644
--- a/theories/Categories/NaturalTransformation/Composition/Core.v
+++ b/theories/Categories/NaturalTransformation/Composition/Core.v
@@ -4,7 +4,9 @@ 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..d98b890c604 100644
--- a/theories/Categories/NaturalTransformation/Composition/Functorial.v
+++ b/theories/Categories/NaturalTransformation/Composition/Functorial.v
@@ -5,7 +5,9 @@ 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..f3122d48284 100644
--- a/theories/Categories/NaturalTransformation/Composition/Laws.v
+++ b/theories/Categories/NaturalTransformation/Composition/Laws.v
@@ -4,7 +4,9 @@ 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..c4234306d1f 100644
--- a/theories/Categories/NaturalTransformation/Core.v
+++ b/theories/Categories/NaturalTransformation/Core.v
@@ -4,7 +4,9 @@ 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..40a50d88ed9 100644
--- a/theories/Categories/NaturalTransformation/Dual.v
+++ b/theories/Categories/NaturalTransformation/Dual.v
@@ -6,7 +6,9 @@ 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..deaefb7dc03 100644
--- a/theories/Categories/NaturalTransformation/Identity.v
+++ b/theories/Categories/NaturalTransformation/Identity.v
@@ -4,7 +4,9 @@ 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..917b400b931 100644
--- a/theories/Categories/NaturalTransformation/Isomorphisms.v
+++ b/theories/Categories/NaturalTransformation/Isomorphisms.v
@@ -10,7 +10,9 @@ 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..f36dcfe7e9f 100644
--- a/theories/Categories/NaturalTransformation/Paths.v
+++ b/theories/Categories/NaturalTransformation/Paths.v
@@ -5,7 +5,9 @@ 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..9a3532cd01d 100644
--- a/theories/Categories/NaturalTransformation/Pointwise.v
+++ b/theories/Categories/NaturalTransformation/Pointwise.v
@@ -6,7 +6,9 @@ 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..4d6c887a6e4 100644
--- a/theories/Categories/NaturalTransformation/Prod.v
+++ b/theories/Categories/NaturalTransformation/Prod.v
@@ -5,7 +5,9 @@ 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..abbf1d7551b 100644
--- a/theories/Categories/NaturalTransformation/Sum.v
+++ b/theories/Categories/NaturalTransformation/Sum.v
@@ -4,7 +4,9 @@ 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..e1cfaaaa9a3 100644
--- a/theories/Categories/ProductLaws.v
+++ b/theories/Categories/ProductLaws.v
@@ -5,7 +5,9 @@ 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..bba649ba0f8 100644
--- a/theories/Categories/Profunctor/Core.v
+++ b/theories/Categories/Profunctor/Core.v
@@ -4,7 +4,9 @@ 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..1cbe9ee911e 100644
--- a/theories/Categories/Profunctor/Identity.v
+++ b/theories/Categories/Profunctor/Identity.v
@@ -4,7 +4,9 @@ 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..e0aa656cff0 100644
--- a/theories/Categories/Profunctor/Representable.v
+++ b/theories/Categories/Profunctor/Representable.v
@@ -4,7 +4,9 @@ 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..367f3f06168 100644
--- a/theories/Categories/Pseudofunctor/Core.v
+++ b/theories/Categories/Pseudofunctor/Core.v
@@ -8,7 +8,9 @@ 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..42fc9830f7e 100644
--- a/theories/Categories/Pseudofunctor/FromFunctor.v
+++ b/theories/Categories/Pseudofunctor/FromFunctor.v
@@ -12,7 +12,9 @@ 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..ed9548e45f5 100644
--- a/theories/Categories/Pseudofunctor/Identity.v
+++ b/theories/Categories/Pseudofunctor/Identity.v
@@ -17,7 +17,9 @@ 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..ad90fa93591 100644
--- a/theories/Categories/Pseudofunctor/RewriteLaws.v
+++ b/theories/Categories/Pseudofunctor/RewriteLaws.v
@@ -12,7 +12,9 @@ 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..fab8a91a0cd 100644
--- a/theories/Categories/PseudonaturalTransformation/Core.v
+++ b/theories/Categories/PseudonaturalTransformation/Core.v
@@ -9,7 +9,9 @@ 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..ac51d13090b 100644
--- a/theories/Categories/SemiSimplicialSets.v
+++ b/theories/Categories/SemiSimplicialSets.v
@@ -10,7 +10,9 @@ 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..274b1f3bcbd 100644
--- a/theories/Categories/SetCategory/Core.v
+++ b/theories/Categories/SetCategory/Core.v
@@ -5,7 +5,9 @@ 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..c9dc9127d91 100644
--- a/theories/Categories/SetCategory/Functors/SetProp.v
+++ b/theories/Categories/SetCategory/Functors/SetProp.v
@@ -5,7 +5,9 @@ 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..8b5221a1d93 100644
--- a/theories/Categories/SetCategory/Morphisms.v
+++ b/theories/Categories/SetCategory/Morphisms.v
@@ -8,7 +8,9 @@ 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..e1a29f427aa 100644
--- a/theories/Categories/SimplicialSets.v
+++ b/theories/Categories/SimplicialSets.v
@@ -9,7 +9,9 @@ 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..7a4f416e687 100644
--- a/theories/Categories/Structure/Core.v
+++ b/theories/Categories/Structure/Core.v
@@ -5,7 +5,9 @@ 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..ab149e36cb5 100644
--- a/theories/Categories/Structure/IdentityPrinciple.v
+++ b/theories/Categories/Structure/IdentityPrinciple.v
@@ -7,7 +7,9 @@ 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..e2094a36fc5 100644
--- a/theories/Categories/UniversalProperties.v
+++ b/theories/Categories/UniversalProperties.v
@@ -13,7 +13,9 @@ 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..129a85c8e3c 100644
--- a/theories/Categories/Yoneda.v
+++ b/theories/Categories/Yoneda.v
@@ -15,7 +15,9 @@ 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.