Skip to content

Adapt to https://github.com/rocq-prover/rocq/pull/21947 #2353

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

Merged
Alizter merged 1 commit into from
Apr 23, 2026
Merged

Adapt to https://github.com/rocq-prover/rocq/pull/21947 #2353

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 1 addition & 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,7 @@
(** ** Pattern Matching *)

(** This flag removes parameters from constructors in patterns that appear in a match statement. *)
Global Set Asymmetric Patterns.
Global Set Asymmetric Patterns. #[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.

(** ** Unification *)

Expand All @@ -52,7 +52,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 55 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
2 changes: 1 addition & 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,7 @@ Require Import Types.Sigma Types.Prod.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope adjunction_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Basics.Tactics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope natural_transformation_scope.

Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Types.Sigma Types.Prod.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope adjunction_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import PathGroupoids HoTT.Tactics Types.Prod Types.Forall.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Ltac law_t :=
rewrite !transport_path_prod'; simpl;
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Adjoint.UnitCounit Adjoint.Core.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope category_scope.

Expand Down
2 changes: 1 addition & 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,7 @@ Require Import HoTT.Types.Prod.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope natural_transformation_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Basics.Tactics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope natural_transformation_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Adjoint.Core Adjoint.UnitCounit Adjoint.Dual.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope natural_transformation_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Functor.Identity.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.


Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Basics.Trunc Types.Sigma HoTT.Tactics Equivalences.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope path_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Adjoint.UnitCounit Adjoint.Core.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
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
2 changes: 1 addition & 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,7 @@ Require Import Basics.Tactics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope morphism_scope.
Local Open Scope natural_transformation_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Basics.PathGroupoids HoTT.Tactics Types.Arrow.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope morphism_scope.
Local Open Scope functor_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Functor.Composition.Core Functor.Identity.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope category_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Basics.Tactics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope natural_transformation_scope.
Local Open Scope category_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import UniversalProperties Comma.Dual InitialTerminalCategory.Core Initi
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope morphism_scope.

Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Functor.Identity Functor.Composition.Core Functor.Composition.Law
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope functor_scope.

Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Category.Morphisms.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope category_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Export Overture Basics.Notations.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Declare Scope morphism_scope.
Declare Scope category_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Category.Core Category.Objects.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.


Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Basics.Equivalences Type
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope category_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Category.Core Category.Morphisms.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope category_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import HoTT.Tactics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope morphism_scope.
Local Open Scope category_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Basics.Trunc.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope category_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Types.Prod.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope category_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Basics.Trunc Types.Sigma.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Notation sig_type := sig.

Expand Down
2 changes: 1 addition & 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,7 @@ Import Functor.Composition.Core.FunctorCompositionCoreNotations.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
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
2 changes: 1 addition & 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,7 @@ Import Functor.Composition.Core.FunctorCompositionCoreNotations.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
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
2 changes: 1 addition & 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,7 @@ Require Import HoTT.Types HoTT.Basics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Notation pr1_type := Overture.pr1 (only parsing).

Expand Down
2 changes: 1 addition & 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,7 @@ Require Export Category.Core.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope morphism_scope.

Expand Down
2 changes: 1 addition & 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,7 @@ Require Export Category.Core.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

(** ** Definition of [+] for categories *)
Section internals.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import HoTT.Basics HoTT.Tactics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope morphism_scope.

Expand Down
2 changes: 1 addition & 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,7 @@ Require Import Functor.Paths.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope functor_scope.

Expand Down
2 changes: 1 addition & 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,7 @@ Require Import HoTT.Basics HoTT.Types.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.


Local Open Scope functor_scope.
Expand Down
2 changes: 1 addition & 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,7 @@ Require Import HoTT.Basics HoTT.Types HoTT.Spaces.Nat.Core.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope nat_scope.

Expand Down
2 changes: 1 addition & 1 deletion theories/Categories/Comma/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ Import Functor.Identity.FunctorIdentityNotations.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.


Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 1 deletion theories/Categories/Comma/Dual.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ Local Set Warnings "notation-overridden".
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope path_scope.
Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 1 deletion theories/Categories/Comma/Functorial.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ Require Import HoTT.Tactics PathGroupoids Types.Forall.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.


Local Open Scope morphism_scope.
Expand Down
2 changes: 1 addition & 1 deletion theories/Categories/Comma/InducedFunctors.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ Require Import Basics.Tactics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope functor_scope.
Local Open Scope category_scope.
Expand Down
2 changes: 1 addition & 1 deletion theories/Categories/Comma/Projection.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Local Set Warnings "notation-overridden". (* work around bug #5567, https://coq.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope functor_scope.
Local Open Scope category_scope.
Expand Down
2 changes: 1 addition & 1 deletion theories/Categories/Comma/ProjectionFunctors.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ Require Import Types.Forall PathGroupoids HoTT.Tactics.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope category_scope.

Expand Down
2 changes: 1 addition & 1 deletion theories/Categories/DependentProduct.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ Require Import CategoryOfSections.Core.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.

Local Open Scope functor_scope.

Expand Down
2 changes: 1 addition & 1 deletion theories/Categories/DiscreteCategory.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ Require Import HoTT.Basics GroupoidCategory.Core.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
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.
Expand Down
Loading
Loading