diff --git a/theories/Basics/Settings.v b/theories/Basics/Settings.v
index 46d7594ebd..2f895e2eff 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 ffaa80735c..decac5e8a8 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 294cfacb51..7e4f0ed75b 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 e7fb2f7510..bab836b001 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 5d224b1268..c6c3cdcb96 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 3b992de31a..99af2b42ff 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 6cf90862ca..b672298121 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 dd841d46bb..d22f5187a1 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 badd5f8087..abfb7fd824 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 940460aeee..dbce1b3aa1 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 5a07618a31..dea732fdf6 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 37c4ec8113..355206469a 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 2a7f6893dc..318415ebe1 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 bee9d590c5..21dc6f4d95 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 d1677a2f11..1172991cd6 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 08711be2cd..a47f42999f 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 e4ef3b2c71..224edbe875 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 a3ad64f3aa..a4a2a4e29b 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 7765a03a37..fb6996a22a 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 3e8ce50db3..4b413b22c4 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 5e3192c588..8ef3725ff9 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 3251a95c15..a0f00952ab 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 2ef90cd787..abc72a5e7b 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 a67240c07e..a89c19d7ea 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 865f58dabb..780220926c 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 683a89d959..c8ba0658dd 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 ca68f449af..74bb1cb7a2 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 c68204e378..835f1e67f4 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 88887409a6..848de59967 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 27d472176f..4412f6fb69 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 5df37fe405..ef85361e79 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 f5e01b8b2b..9de227d5f4 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 c1bd4c88b8..950b0b6e22 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 f019a1eb14..e66131d6c8 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 98bf9cea10..1e607d3b07 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 85af68c94c..9642c0826a 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 48d37629c8..1e5f6681dd 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 e3b4a05e9d..bad79776e4 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 4463fcf748..4a77516040 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 bf0fab941b..5441d1cec5 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 0a682aa381..78f97655e5 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 6702d7f67a..271590f400 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 438aad41dd..a6e3d856ec 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 60e2c94af7..2e10a6ae9e 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 d5a36d990b..7f9775422a 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 e6704a81a8..1dfe7f33c5 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 4cf798facb..9e41b3e920 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 8ce178f169..5e5193cf22 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 5d10cc5859..b63b8e522d 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 169938590e..484d6d8cac 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 2fc051b639..fe8ef14e32 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 7eac2c714c..bfa05262ca 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 ca7fe03569..14107106d7 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 b957d2d2de..0605ff9d19 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 209c054ee4..b4a20ec10c 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 ef8848e973..eab48b6669 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 be9802e05d..c906514583 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 1dceced2fe..62044d6dcd 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 90231b5924..addcff84a6 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 ac90a126dd..3662bb83bf 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 f7f73df5a0..36676db4dd 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 f823512ade..9116d16f63 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 18503710d5..79adb66b6a 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 2d94a02a6c..d55c28d2fe 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 64407740b8..0fcde0bc2f 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 bb3e703d5e..4da1b230a7 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 26a898e5f9..45a8579cc0 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 df1ad2d92e..6beb025b08 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 7f90d0905b..7d58a04751 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 15896afa5d..20ea1fd9f5 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 10e6623164..5012aa160b 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 51f6103137..fbfc62be7f 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 396dfee5e2..467ba2f449 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 c2cbfa69c6..a14f609383 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 973cc74307..a253ab12cb 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 839a13ed1f..dc968e25e6 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 2182f73f99..da847c19e6 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 384a2ebbfc..2fb6acfac5 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 315a6a9003..f4d31d39e5 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 d9311baf79..15de726da7 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 12e1594e9c..0bdb572fcb 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 2ac8962053..a51b229b9e 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 18f75e0b9e..481ab6823b 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 c125dc3f66..07c2a69f70 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 6181418894..a2245e9bec 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 11ca76691e..50772ebafa 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 bafaeae0bc..95b8b5ce0d 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 f10cbaace7..0a5b8dc805 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 6b49f56418..79909d25c5 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 8873096815..b8d48f3f8e 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 996045f6e6..34a2b30da1 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 1c5ffbe660..b2f96c5364 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 9acd60b351..915d7bf5d1 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 399d1d93cf..e59f1168e3 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 a0defc270e..d9c9368904 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 736b2dfcdc..d413f275c2 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 3dd7cc345b..65172ed899 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 fcb9c47dac..1641c1ea49 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 b5b867f027..4ded6cd125 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 b914bd3b6d..d98b890c60 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 152fb81c0e..f3122d4828 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 5a03a059ba..c4234306d1 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 f88ae049fb..40a50d88ed 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 47725b2ae5..deaefb7dc0 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 51bbb64cd5..917b400b93 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 550d734ce5..f36dcfe7e9 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 8f6e583188..9a3532cd01 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 8da27e1367..4d6c887a6e 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 10a77278de..abbf1d7551 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 6a62b0168b..e1cfaaaa9a 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 fd2c1f5cd5..bba649ba0f 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 8b5e4426b3..1cbe9ee911 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 4d3145b0b4..e0aa656cff 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 3fe4af3dea..367f3f0616 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 65281cf542..42fc9830f7 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 36c81072e0..ed9548e45f 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 767cf2cd4b..ad90fa9359 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 4db9628e73..fab8a91a0c 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 7e54de2095..ac51d13090 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 cd2fb4838f..274b1f3bcb 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 080bfe25c4..c9dc9127d9 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 9007087bc5..8b5221a1d9 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 3a7dce5c22..e1a29f427a 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 1d5d6ed904..7a4f416e68 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 c6c2397c92..ab149e36cb 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 390852f495..e2094a36fc 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 c7d76f9578..129a85c8e3 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.