chore: put asymmetric patterns commands on separate lines

theories/Basics/Settings.v

@@ -42,7 +42,10 @@
 (** ** 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 *)
 
@@ -52,7 +55,7 @@
 (** ** Typeclasses and Hint settings *)
 
 (** This tells Coq that when we [Require] a module without [Import]ing it, typeclass instances defined in that module should also not be imported.  In other words, the only effect of [Require] without [Import] is to make qualified names available. *)
 Global Set Loose Hint Behavior "Strict".
 
 Create HintDb rewrite discriminated.
 #[export] Hint Variables Opaque : rewrite.

theories/Categories/Adjoint/Composition/AssociativityLaw.v

@@ -4,10 +4,8 @@ Require Import Adjoint.Composition.Core Adjoint.Core.
 Require Adjoint.Composition.LawsTactic.
 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.
 
 Local Open Scope adjunction_scope.
 Local Open Scope morphism_scope.

theories/Categories/Adjoint/Composition/Core.v

@@ -7,10 +7,8 @@ Require Import Adjoint.UnitCounit Adjoint.Core.
 Require Import HoTT.Tactics.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 

theories/Categories/Adjoint/Composition/IdentityLaws.v

@@ -4,10 +4,8 @@ Require Import Adjoint.Composition.Core Adjoint.Core Adjoint.Identity.
 Require Adjoint.Composition.LawsTactic.
 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.
 
 Local Open Scope adjunction_scope.
 Local Open Scope morphism_scope.

theories/Categories/Adjoint/Composition/LawsTactic.v

@@ -4,10 +4,8 @@ Require Import Functor.Composition.Laws.
 Require Import Adjoint.UnitCounit Adjoint.Paths.
 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.
 
 Ltac law_t :=
   rewrite !transport_path_prod'; simpl;

theories/Categories/Adjoint/Dual.v

@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core.
 Require Import Functor.Dual NaturalTransformation.Dual.
 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.
 
 Local Open Scope category_scope.
 

theories/Categories/Adjoint/Functorial/Core.v

@@ -7,10 +7,8 @@ Require Import Adjoint.Core.
 Require Import Adjoint.Functorial.Parts Adjoint.Functorial.Laws.
 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.
 
 Local Open Scope natural_transformation_scope.
 Local Open Scope morphism_scope.

theories/Categories/Adjoint/Functorial/Laws.v

@@ -10,10 +10,8 @@ Require Import Adjoint.Functorial.Parts.
 Require Import HoTT.Tactics.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 Local Open Scope morphism_scope.

theories/Categories/Adjoint/Functorial/Parts.v

@@ -5,10 +5,8 @@ Require Import NaturalTransformation.Composition.Core NaturalTransformation.Comp
 Require Import Functor.Dual NaturalTransformation.Dual.
 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.
 
 Local Open Scope natural_transformation_scope.
 Local Open Scope morphism_scope.

theories/Categories/Adjoint/Hom.v

@@ -8,11 +8,8 @@ Require Import Functor.Composition.Core.
 Require Import FunctorCategory.Morphisms.
 Require Import Functor.Identity.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
 
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.

theories/Categories/Adjoint/HomCoercions.v

@@ -8,10 +8,8 @@ Require Import Functor.Identity.
 Require Import SetCategory.Morphisms.
 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.
 
 Local Open Scope path_scope.
 Local Open Scope morphism_scope.

theories/Categories/Adjoint/Identity.v

@@ -3,10 +3,8 @@ Require Import Category.Core.
 Require Import Functor.Identity NaturalTransformation.Identity.
 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.
 
 Section identity.
   (** There is an identity adjunction.  It does the obvious thing. *)

theories/Categories/Adjoint/Paths.v

@@ -5,10 +5,8 @@ Require Import Adjoint.UnitCounit Adjoint.Core NaturalTransformation.Paths.
 Require Import Types Trunc.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 Local Open Scope natural_transformation_scope.
@@ -20,8 +18,6 @@ Section path_adjunction.
   Variable F : Functor C D.
   Variable G : Functor D C.
 
-
-
   Notation adjunction_sig :=
     { eta : NaturalTransformation 1 (G o F)
     | { eps : NaturalTransformation (F o G) 1

theories/Categories/Adjoint/Pointwise.v

@@ -12,10 +12,8 @@ Import NaturalTransformation.Identity.NaturalTransformationIdentityNotations.
 Require Import NaturalTransformation.Paths Functor.Paths.
 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.
 
 Local Open Scope morphism_scope.
 Local Open Scope functor_scope.

theories/Categories/Adjoint/UnitCounit.v

@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core NaturalTransformation.Core.
 Require Import Category.Dual Functor.Dual NaturalTransformation.Dual.
 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.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.

theories/Categories/Adjoint/UnitCounitCoercions.v

@@ -5,10 +5,8 @@ Require Import Functor.Composition.Core Functor.Identity.
 Require Import HoTT.Tactics Basics.Trunc Types.Sigma.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 Local Open Scope category_scope.

theories/Categories/Adjoint/UniversalMorphisms/Core.v

@@ -9,10 +9,8 @@ Import Comma.Core.
 Local Set Warnings "notation-overridden".
 Require Import UniversalProperties Comma.Dual InitialTerminalCategory.Core InitialTerminalCategory.Functors.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 

theories/Categories/Cat/Core.v

@@ -2,10 +2,8 @@
 Require Import Category.Objects InitialTerminalCategory.Core InitialTerminalCategory.Functors Functor.Core Category.Strict Functor.Paths.
 Require Import Functor.Identity Functor.Composition.Core Functor.Composition.Laws.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 

theories/Categories/Cat/Morphisms.v

@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core FunctorCategory.Core NaturalTransformation.Core.
 Require Import Category.Morphisms.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.

theories/Categories/Category/Core.v

@@ -1,10 +1,8 @@
 (** * Definition of a [PreCategory] *)
 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.
 
 Declare Scope morphism_scope.
 Declare Scope category_scope.

theories/Categories/Category/Dual.v

@@ -1,11 +1,8 @@
 (** * Opposite Category *)
 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.
-
 
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.

theories/Categories/Category/Morphisms.v

@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core.
 Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Basics.Equivalences Types.Sigma.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.

theories/Categories/Category/Objects.v

@@ -2,10 +2,8 @@
 Require Import Basics.Contractible.
 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.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.

theories/Categories/Category/Paths.v

@@ -4,18 +4,14 @@ Require Import HoTT.Basics.Equivalences HoTT.Basics.PathGroupoids HoTT.Basics.Tr
 Require Import HoTT.Types.Sigma HoTT.Types.Arrow HoTT.Types.Forall.
 Require Import HoTT.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.
 
 Section path_category.
   Local Open Scope path_scope.
-
-
   (** We add a prime ([']) as an arbitrary convention to denote that
       we are talking about equality of functions (less convenient for
       use) rather than pointwise equality of functions (more

theories/Categories/Category/Pi.v

@@ -2,10 +2,8 @@
 Require Import Category.Strict.
 Require Import Basics.Trunc.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.

theories/Categories/Category/Prod.v

@@ -3,10 +3,8 @@ Require Import Basics.Tactics.
 Require Import Category.Strict.
 Require Import Types.Prod.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.

theories/Categories/Category/Sigma/Core.v

@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core.
 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.
 
 Local Notation sig_type := sig.
 

theories/Categories/Category/Sigma/OnMorphisms.v

@@ -6,10 +6,8 @@ Require Import Functor.Paths.
 Import Functor.Identity.FunctorIdentityNotations.
 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.
 
 Local Notation sig_type := Overture.sig.
 Local Notation pr1_type := Overture.pr1.

theories/Categories/Category/Sigma/OnObjects.v

@@ -6,10 +6,8 @@ Require Import Functor.Paths.
 Import Functor.Identity.FunctorIdentityNotations.
 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.
 
 Local Notation sig_type := Overture.sig.
 Local Notation pr1_type := Overture.pr1.

theories/Categories/Category/Sigma/Univalent.v

@@ -4,10 +4,8 @@ Require Import Category.Univalent.
 Require Import Category.Sigma.Core Category.Sigma.OnObjects Category.Sigma.OnMorphisms.
 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.
 
 Local Notation pr1_type := Overture.pr1 (only parsing).
 

theories/Categories/Category/Strict.v

@@ -1,10 +1,8 @@
 (** * Definition of a strict category *)
 Require Export Category.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 

theories/Categories/Category/Sum.v

@@ -1,10 +1,8 @@
 (** * The coproduct of categories *)
 Require Export Category.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** ** Definition of [+] for categories *)
 Section internals.

theories/Categories/Category/Univalent.v

@@ -2,10 +2,8 @@
 Require Import Category.Core Category.Morphisms.
 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.
 
 Local Open Scope morphism_scope.
 

theories/Categories/CategoryOfGroupoids.v

@@ -4,10 +4,8 @@ Require Import Cat.Core.
 Require Import GroupoidCategory.Core.
 Require Import Functor.Paths.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.