Skip to content

Fix style: split asymmetric patterns commands onto separate lines #2354

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Closed
Copilot wants to merge 2 commits into from
Closed

Fix style: split asymmetric patterns commands onto separate lines #2354

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0f1cab7
Fix style issues from #2353: split two commands onto separate lines
Copilot Apr 24, 2026
fa220fc
Further style fixes: put warning attribute on its own line; add versi…
Copilot Apr 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion theories/Basics/Settings.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)

Expand All @@ -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".

Check warning on line 58 in theories/Basics/Settings.v

View workflow job for this annotation

GitHub Actions / opam-build (dev, ubuntu-latest) 

There is no flag or option with this name: "Loose Hint Behavior".

Check warning on line 58 in theories/Basics/Settings.v

View workflow job for this annotation

GitHub Actions / opam-build (dev, ubuntu-latest) 

There is no flag or option with this name: "Loose Hint Behavior".

Create HintDb rewrite discriminated.
#[export] Hint Variables Opaque : rewrite.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Composition/AssociativityLaw.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Composition/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Composition/IdentityLaws.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Composition/LawsTactic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Dual.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Functorial/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Functorial/Laws.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Functorial/Parts.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Hom.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/HomCoercions.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Identity.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Paths.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/Pointwise.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/UnitCounit.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/UnitCounitCoercions.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Adjoint/UniversalMorphisms/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Cat/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Cat/Morphisms.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Dual.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Morphisms.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Objects.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Paths.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Pi.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Prod.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Sigma/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Sigma/OnMorphisms.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Sigma/OnObjects.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Sigma/Univalent.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).

Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Strict.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Sum.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/Category/Univalent.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/CategoryOfGroupoids.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/CategoryOfSections/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 3 additions & 1 deletion theories/Categories/ChainCategory.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
Loading
Loading