From 6b07450b0a273aa11d44bdb57ea579f57bb8c140 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Mon, 19 Feb 2024 02:39:57 +0000 Subject: [PATCH] [8.19] fix % in Arguments warnings Signed-off-by: Ali Caglayan --- theories/Algebra/Universal/Algebra.v | 8 ++-- theories/Algebra/Universal/Homomorphism.v | 2 +- theories/Basics/Equivalences.v | 6 +-- theories/Basics/Nat.v | 4 +- theories/Basics/Overture.v | 40 +++++++++---------- theories/Basics/Settings.v | 4 -- theories/Categories/Adjoint/Hom.v | 2 +- theories/Categories/Adjoint/UnitCounit.v | 10 ++--- theories/Categories/Category/Core.v | 8 ++-- theories/Categories/Functor/Core.v | 4 +- .../Categories/NaturalTransformation/Core.v | 4 +- theories/Categories/Pseudofunctor/Core.v | 4 +- .../PseudonaturalTransformation/Core.v | 4 +- theories/Extensions.v | 4 +- theories/Homotopy/Join/Core.v | 6 +-- theories/Homotopy/Join/TriJoin.v | 6 +-- theories/Homotopy/Suspension.v | 2 +- theories/Limits/Pullback.v | 2 +- theories/Modalities/ReflectiveSubuniverse.v | 12 +++--- theories/Spaces/BinInt/Core.v | 2 +- theories/Types/Forall.v | 6 +-- theories/Types/Universe.v | 2 +- theories/WildCat/Core.v | 6 +-- theories/WildCat/Equiv.v | 10 ++--- 24 files changed, 77 insertions(+), 81 deletions(-) diff --git a/theories/Algebra/Universal/Algebra.v b/theories/Algebra/Universal/Algebra.v index a7c6c624736..ba410610c96 100644 --- a/theories/Algebra/Universal/Algebra.v +++ b/theories/Algebra/Universal/Algebra.v @@ -116,7 +116,7 @@ Proof. exact q. Defined. -Arguments path_algebra {_} {_} (A B)%Algebra_scope (p q)%path_scope. +Arguments path_algebra {_} {_} (A B)%_Algebra_scope (p q)%_path_scope. Lemma path_ap_carriers_path_algebra `{Funext} {σ} (A B : Algebra σ) (p : carriers A = carriers B) @@ -131,7 +131,7 @@ Proof. now destruct (center (ha = hb)). Defined. -Arguments path_ap_carriers_path_algebra {_} {_} (A B)%Algebra_scope (p q)%path_scope. +Arguments path_ap_carriers_path_algebra {_} {_} (A B)%_Algebra_scope (p q)%_path_scope. Lemma path_path_algebra_issig {σ : Signature} {A B : Algebra σ} (p q : A = B) (r : ap (issig_algebra σ)^-1 p = ap (issig_algebra σ)^-1 q) @@ -141,7 +141,7 @@ Proof. by apply (@equiv_inv _ _ (ap e) (Equivalences.isequiv_ap _ _)). Defined. -Arguments path_path_algebra_issig {_} {A B}%Algebra_scope (p q r)%path_scope. +Arguments path_path_algebra_issig {_} {A B}%_Algebra_scope (p q r)%_path_scope. Lemma path_path_algebra `{Funext} {σ} {A B : Algebra σ} (p q : A = B) (r : ap carriers p = ap carriers q) @@ -154,6 +154,6 @@ Proof. - apply path_ishprop. Defined. -Arguments path_path_algebra {_} {σ} {A B}%Algebra_scope (p q r)%path_scope. +Arguments path_path_algebra {_} {σ} {A B}%_Algebra_scope (p q r)%_path_scope. Global Notation "u .# A" := (operations A u) : Algebra_scope. diff --git a/theories/Algebra/Universal/Homomorphism.v b/theories/Algebra/Universal/Homomorphism.v index 53e2e47189d..7e39a877131 100644 --- a/theories/Algebra/Universal/Homomorphism.v +++ b/theories/Algebra/Universal/Homomorphism.v @@ -98,7 +98,7 @@ Section homomorphism_id. End homomorphism_id. -Arguments homomorphism_id {σ} A%Algebra_scope , {σ} {A}. +Arguments homomorphism_id {σ} A%_Algebra_scope , {σ} {A}. (** Composition of homomorphisms. *) diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v index 1c04e560467..c3595a04390 100644 --- a/theories/Basics/Equivalences.v +++ b/theories/Basics/Equivalences.v @@ -133,8 +133,8 @@ Section Adjointify. End Adjointify. -Arguments isequiv_adjointify {A B}%type_scope (f g)%function_scope isretr issect. -Arguments equiv_adjointify {A B}%type_scope (f g)%function_scope isretr issect. +Arguments isequiv_adjointify {A B}%_type_scope (f g)%_function_scope isretr issect. +Arguments equiv_adjointify {A B}%_type_scope (f g)%_function_scope isretr issect. (** Anything homotopic to an equivalence is an equivalence. This should not be an instance; it can cause the unifier to spin forever searching for functions to be homotopic to. *) Definition isequiv_homotopic {A B : Type} (f : A -> B) {g : A -> B} @@ -283,7 +283,7 @@ Definition equiv_ap `(f : A -> B) `{IsEquiv A B f} (x y : A) : (x = y) <~> (f x = f y) := Build_Equiv _ _ (ap f) _. -Global Arguments equiv_ap (A B)%type_scope f%function_scope _ _ _. +Global Arguments equiv_ap (A B)%_type_scope f%_function_scope _ _ _. Definition equiv_ap' `(f : A <~> B) (x y : A) : (x = y) <~> (f x = f y) diff --git a/theories/Basics/Nat.v b/theories/Basics/Nat.v index 973a18118c1..7ad83359571 100644 --- a/theories/Basics/Nat.v +++ b/theories/Basics/Nat.v @@ -110,8 +110,8 @@ Definition to_int n := Decimal.Pos (to_uint n). Definition to_num_int n := Numeral.IntDec (to_int n). -Arguments of_uint d%dec_uint_scope. -Arguments of_int d%dec_int_scope. +Arguments of_uint d%_dec_uint_scope. +Arguments of_int d%_dec_int_scope. (* Parsing / printing of [nat] numbers *) Number Notation nat of_num_uint to_num_uint (abstract after 5001) : nat_scope. diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index 228d099c048..c49937bf24a 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -172,11 +172,11 @@ Arguments sig_ind {_ _}. (** We make the parameters maximally inserted so that we can pass around [pr1] as a function and have it actually mean "first projection" in, e.g., [ap]. *) -Arguments exist {A}%type P%type _ _. +Arguments exist {A}%_type P%_type _ _. Arguments proj1 {A P} _ / . Arguments proj2 {A P} _ / . -Arguments sig (A P)%type. +Arguments sig (A P)%_type. Notation "{ x | P }" := (sig (fun x => P)) : type_scope. Notation "{ x : A | P }" := (sig (A := A) (fun x => P)) : type_scope. @@ -239,7 +239,7 @@ Global Instance iff_reflexive : Reflexive iff | 1 (** Dependent composition of functions. *) Definition composeD {A B C} (g : forall b, C b) (f : A -> B) := fun x : A => g (f x). -Global Arguments composeD {A B C}%type_scope (g f)%function_scope x. +Global Arguments composeD {A B C}%_type_scope (g f)%_function_scope x. #[export] Hint Unfold composeD : core. @@ -369,7 +369,7 @@ Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) := match p with idpath => u end. (** See above for the meaning of [simpl nomatch]. *) -Arguments transport {A}%type_scope P%function_scope {x y} p%path_scope u : simpl nomatch. +Arguments transport {A}%_type_scope P%_function_scope {x y} p%_path_scope u : simpl nomatch. (** Transport is very common so it is worth introducing a parsing notation for it. However, we do not use the notation for output because it hides the fibration, and so makes it very hard to read involved transport expression. *) Notation "p # x" := (transport _ p x) (only parsing) : path_scope. @@ -382,8 +382,8 @@ Proof. rewrite <- H. exact u. Defined. Local Lemma define_internal_paths_rew_r A x y P (u : P y) (H : x = y :> A) : P x. Proof. rewrite -> H. exact u. Defined. -Arguments internal_paths_rew {A%type_scope} {a} P%function_scope f {a0} p. -Arguments internal_paths_rew_r {A%type_scope} {a y} P%function_scope HC X. +Arguments internal_paths_rew {A%_type_scope} {a} P%_function_scope f {a0} p. +Arguments internal_paths_rew_r {A%_type_scope} {a y} P%_function_scope HC X. (** Having defined transport, we can use it to talk about what a homotopy theorist might see as "paths in a fibration over paths in the base"; and what a type theorist might see as "heterogeneous equality in a dependent type". We will first see this appearing in the type of [apD]. *) @@ -392,7 +392,7 @@ Arguments internal_paths_rew_r {A%type_scope} {a y} P%function_scope HC X. Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. -Global Arguments ap {A B}%type_scope f%function_scope {x y} p%path_scope. +Global Arguments ap {A B}%_type_scope f%_function_scope {x y} p%_path_scope. Register ap as core.identity.congr. @@ -426,7 +426,7 @@ Proof. intros ? ? p ?; symmetry; apply p. Defined. -Global Arguments pointwise_paths {A}%type_scope {P} (f g)%function_scope. +Global Arguments pointwise_paths {A}%_type_scope {P} (f g)%_function_scope. Global Arguments reflexive_pointwise_paths /. Global Arguments transitive_pointwise_paths /. Global Arguments symmetric_pointwise_paths /. @@ -440,12 +440,12 @@ Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g) : f == g := fun x => match h with idpath => 1 end. -Global Arguments apD10 {A%type_scope B} {f g}%function_scope h%path_scope _. +Global Arguments apD10 {A%_type_scope B} {f g}%_function_scope h%_path_scope _. Definition ap10 {A B} {f g:A->B} (h:f=g) : f == g := apD10 h. -Global Arguments ap10 {A B}%type_scope {f g}%function_scope h%path_scope _. +Global Arguments ap10 {A B}%_type_scope {f g}%_function_scope h%_path_scope _. (** For the benefit of readers of the HoTT Book: *) Notation happly := ap10 (only parsing). @@ -455,7 +455,7 @@ Proof. case h, p; reflexivity. Defined. -Global Arguments ap11 {A B}%type_scope {f g}%function_scope h%path_scope {x y} p%path_scope. +Global Arguments ap11 {A B}%_type_scope {f g}%_function_scope h%_path_scope {x y} p%_path_scope. (** See above for the meaning of [simpl nomatch]. *) Arguments ap {A B} f {x y} p : simpl nomatch. @@ -470,7 +470,7 @@ Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): match p with idpath => idpath end. (** See above for the meaning of [simpl nomatch]. *) -Arguments apD {A%type_scope B} f%function_scope {x y} p%path_scope : simpl nomatch. +Arguments apD {A%_type_scope B} f%_function_scope {x y} p%_path_scope : simpl nomatch. (** ** Equivalences *) @@ -496,10 +496,10 @@ Class IsEquiv {A B : Type} (f : A -> B) := { eisadj : forall x : A, eisretr (f x) = ap f (eissect x) ; }. -Arguments eisretr {A B}%type_scope f%function_scope {_} _. -Arguments eissect {A B}%type_scope f%function_scope {_} _. -Arguments eisadj {A B}%type_scope f%function_scope {_} _. -Arguments IsEquiv {A B}%type_scope f%function_scope. +Arguments eisretr {A B}%_type_scope f%_function_scope {_} _. +Arguments eissect {A B}%_type_scope f%_function_scope {_} _. +Arguments eisadj {A B}%_type_scope f%_function_scope {_} _. +Arguments IsEquiv {A B}%_type_scope f%_function_scope. (** We mark [eisadj] as Opaque to deter Coq from unfolding it when simplifying. Since proofs of [eisadj] typically have larger proofs than the rest of the equivalence data, we gain some speed up as a result. *) Global Opaque eisadj. @@ -566,7 +566,7 @@ Definition trunc_index_rect := trunc_index_ind. (** We will use [Notation] for [trunc_index]es, so define a scope for them here. *) Bind Scope trunc_scope with trunc_index. -Arguments trunc_S _%trunc_scope. +Arguments trunc_S _%_trunc_scope. (** Include the basic numerals, so we don't need to go through the coercion from [nat], and so that we get the right binding with [trunc_scope]. *) (** Note that putting the negative numbers at level 0 allows us to override the [- _] notation for negative numbers. *) @@ -679,7 +679,7 @@ Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, := (@apD10 A P f g)^-1. -Global Arguments path_forall {_ A%type_scope P} (f g)%function_scope _. +Global Arguments path_forall {_ A%_type_scope P} (f g)%_function_scope _. (** *** Tactics *) @@ -719,7 +719,7 @@ Scheme nat_rec := Minimality for nat Sort Type. Declare Scope nat_scope. Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. -Arguments S _%nat. +Arguments S _%_nat. (** We put [Empty] here, instead of in [Empty.v], because [Ltac done] uses it. *) Inductive Empty : Type0 := . @@ -790,4 +790,4 @@ Global Existing Instance ispointed_type. Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }. -Global Arguments hfiber {A B}%type_scope f%function_scope y. +Global Arguments hfiber {A B}%_type_scope f%_function_scope y. diff --git a/theories/Basics/Settings.v b/theories/Basics/Settings.v index be2431f1273..cb5d6d46745 100644 --- a/theories/Basics/Settings.v +++ b/theories/Basics/Settings.v @@ -4,10 +4,6 @@ (** ** Warnings *) -(* TODO: remove this once we bump the minimal Coq version to 8.19 and merge #1862. *) -(** Disable warning about argument scope delimiters. *) -Global Set Warnings "-argument-scope-delimiter". - (** ** Plugins *) (** Load the Ltac plugin. This is the tactic language we use for proofs. *) diff --git a/theories/Categories/Adjoint/Hom.v b/theories/Categories/Adjoint/Hom.v index c8d94995f24..1e04a627a9d 100644 --- a/theories/Categories/Adjoint/Hom.v +++ b/theories/Categories/Adjoint/Hom.v @@ -84,4 +84,4 @@ End Adjunction. Coercion mate_of : AdjunctionHom >-> NaturalIsomorphism. Bind Scope adjunction_scope with AdjunctionHom. -Arguments mate_of {_} [C%category D%category F%functor G%functor] _%adjunction. +Arguments mate_of {_} [C%_category D%_category F%_functor G%_functor] _%_adjunction. diff --git a/theories/Categories/Adjoint/UnitCounit.v b/theories/Categories/Adjoint/UnitCounit.v index a5b7bc2ecc3..0212926a386 100644 --- a/theories/Categories/Adjoint/UnitCounit.v +++ b/theories/Categories/Adjoint/UnitCounit.v @@ -283,8 +283,8 @@ Bind Scope adjunction_scope with AdjunctionUnit. Bind Scope adjunction_scope with AdjunctionCounit. Bind Scope adjunction_scope with AdjunctionUnitCounit. -Arguments unit [C D]%category [F G]%functor _%adjunction / . -Arguments counit [C D]%category [F G]%functor _%adjunction / . -Arguments AdjunctionUnitCounit [C D]%category (F G)%functor. -Arguments unit_counit_equation_1 [C D]%category [F G]%functor _%adjunction _%object. -Arguments unit_counit_equation_2 [C D]%category [F G]%functor _%adjunction _%object. +Arguments unit [C D]%_category [F G]%_functor _%_adjunction / . +Arguments counit [C D]%_category [F G]%_functor _%_adjunction / . +Arguments AdjunctionUnitCounit [C D]%_category (F G)%_functor. +Arguments unit_counit_equation_1 [C D]%_category [F G]%_functor _%_adjunction _%_object. +Arguments unit_counit_equation_2 [C D]%_category [F G]%_functor _%_adjunction _%_object. diff --git a/theories/Categories/Category/Core.v b/theories/Categories/Category/Core.v index 56766135f00..08a05c04888 100644 --- a/theories/Categories/Category/Core.v +++ b/theories/Categories/Category/Core.v @@ -79,10 +79,10 @@ Bind Scope object_scope with object. Bind Scope morphism_scope with morphism. (** We want eta-expanded primitive projections to [simpl] away. *) -Arguments object !C%category / : rename. -Arguments morphism !C%category / s d : rename. -Arguments identity {!C%category} / x%object : rename. -Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename. +Arguments object !C%_category / : rename. +Arguments morphism !C%_category / s d : rename. +Arguments identity {!C%_category} / x%_object : rename. +Arguments compose {!C%_category} / {s d d'}%_object (m1 m2)%_morphism : rename. Local Infix "o" := compose : morphism_scope. (** Perhaps we should consider making this notation more global. *) diff --git a/theories/Categories/Functor/Core.v b/theories/Categories/Functor/Core.v index afbe31582e6..6073f75d28a 100644 --- a/theories/Categories/Functor/Core.v +++ b/theories/Categories/Functor/Core.v @@ -47,8 +47,8 @@ Bind Scope functor_scope with Functor. Create HintDb functor discriminated. Arguments Functor C D : assert. -Arguments object_of {C%category D%category} F%functor c%object : rename, simpl nomatch. -Arguments morphism_of [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. +Arguments object_of {C%_category D%_category} F%_functor c%_object : rename, simpl nomatch. +Arguments morphism_of [C%_category] [D%_category] F%_functor [s%_object d%_object] m%_morphism : rename, simpl nomatch. Arguments composition_of [C D] F _ _ _ _ _ : rename. Arguments identity_of [C D] F _ : rename. diff --git a/theories/Categories/NaturalTransformation/Core.v b/theories/Categories/NaturalTransformation/Core.v index 038dbe09721..cc189cd9a8b 100644 --- a/theories/Categories/NaturalTransformation/Core.v +++ b/theories/Categories/NaturalTransformation/Core.v @@ -59,8 +59,8 @@ Bind Scope natural_transformation_scope with NaturalTransformation. Create HintDb natural_transformation discriminated. -Global Arguments components_of {C D}%category {F G}%functor T%natural_transformation / - c%object : rename. +Global Arguments components_of {C D}%_category {F G}%_functor T%_natural_transformation / + c%_object : rename. Global Arguments commutes {C D F G} !T / _ _ _ : rename. Global Arguments commutes_sym {C D F G} !T / _ _ _ : rename. diff --git a/theories/Categories/Pseudofunctor/Core.v b/theories/Categories/Pseudofunctor/Core.v index 5b41c590496..e988525a591 100644 --- a/theories/Categories/Pseudofunctor/Core.v +++ b/theories/Categories/Pseudofunctor/Core.v @@ -194,8 +194,8 @@ Bind Scope pseudofunctor_scope with Pseudofunctor. Create HintDb pseudofunctor discriminated. -Arguments p_object_of {_} {C%category} F%pseudofunctor / c%object : rename. -Arguments p_morphism_of {_} {C%category} F%pseudofunctor / {s d}%object m%morphism : rename. +Arguments p_object_of {_} {C%_category} F%_pseudofunctor / c%_object : rename. +Arguments p_morphism_of {_} {C%_category} F%_pseudofunctor / {s d}%_object m%_morphism : rename. (*Notation "F ₀ x" := (p_object_of F x) : object_scope. Notation "F ₁ m" := (p_morphism_of F m) : morphism_scope.*) diff --git a/theories/Categories/PseudonaturalTransformation/Core.v b/theories/Categories/PseudonaturalTransformation/Core.v index 7f03f17dfe2..60a52510296 100644 --- a/theories/Categories/PseudonaturalTransformation/Core.v +++ b/theories/Categories/PseudonaturalTransformation/Core.v @@ -221,8 +221,8 @@ Bind Scope pseudonatural_transformation_scope with PseudonaturalTransformation. Create HintDb pseuodnatural_transformation discriminated. -Arguments p_components_of {_} {X}%category {F G}%pseudofunctor T%pseudonatural_transformation - a%object : rename, simpl nomatch. +Arguments p_components_of {_} {X}%_category {F G}%_pseudofunctor T%_pseudonatural_transformation + a%_object : rename, simpl nomatch. #[export] Hint Resolve p_commutes_respects_identity p_commutes_respects_composition : category pseudonatural_transformation. diff --git a/theories/Extensions.v b/theories/Extensions.v index 479ec44c720..bacb14cba98 100644 --- a/theories/Extensions.v +++ b/theories/Extensions.v @@ -102,7 +102,7 @@ Section Extensions. - size of C - size of result (>= A,B,C) *) - Global Arguments ExtendableAlong n%nat_scope {A B}%type_scope (f C)%function_scope. + Global Arguments ExtendableAlong n%_nat_scope {A B}%_type_scope (f C)%_function_scope. (** We can modify the universes, as with [ExtensionAlong]. *) Definition lift_extendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} @@ -324,7 +324,7 @@ Section Extensions. := forall n : nat, ExtendableAlong@{i j k l} n f C. (** Universe parameters are the same as for [ExtendableAlong]. *) - Global Arguments ooExtendableAlong {A B}%type_scope (f C)%function_scope. + Global Arguments ooExtendableAlong {A B}%_type_scope (f C)%_function_scope. (** Universe modification. *) Definition lift_ooextendablealong@{a1 a2 amin b1 b2 bmin p1 p2 pmin m1 m2} diff --git a/theories/Homotopy/Join/Core.v b/theories/Homotopy/Join/Core.v index e0d22f14fd6..c6c480aa472 100644 --- a/theories/Homotopy/Join/Core.v +++ b/theories/Homotopy/Join/Core.v @@ -92,8 +92,8 @@ Section Join. End Join. -Arguments joinl {A B}%type_scope _ , [A] B _. -Arguments joinr {A B}%type_scope _ , A [B] _. +Arguments joinl {A B}%_type_scope _ , [A] B _. +Arguments joinr {A B}%_type_scope _ , A [B] _. (** * [Join_rec] gives an equivalence of 0-groupoids @@ -106,7 +106,7 @@ Record JoinRecData {A B P : Type} := { }. Arguments JoinRecData : clear implicits. -Arguments Build_JoinRecData {A B P}%type_scope (jl jr jg)%function_scope. +Arguments Build_JoinRecData {A B P}%_type_scope (jl jr jg)%_function_scope. (** We use the name [join_rec] for the version of [Join_rec] defined on this data. *) Definition join_rec {A B P : Type} (f : JoinRecData A B P) diff --git a/theories/Homotopy/Join/TriJoin.v b/theories/Homotopy/Join/TriJoin.v index 0a92aaefa8e..52bab840645 100644 --- a/theories/Homotopy/Join/TriJoin.v +++ b/theories/Homotopy/Join/TriJoin.v @@ -156,7 +156,7 @@ Record TriJoinRecData {A B C P : Type} := { }. Arguments TriJoinRecData : clear implicits. -Arguments Build_TriJoinRecData {A B C P}%type_scope (j1 j2 j3 j12 j13 j23 j123)%function_scope. +Arguments Build_TriJoinRecData {A B C P}%_type_scope (j1 j2 j3 j12 j13 j23 j123)%_function_scope. Definition trijoin_rec {A B C P : Type} (f : TriJoinRecData A B C P) : TriJoin A B C $-> P. @@ -297,8 +297,8 @@ Record TriJoinRecData' {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C - }. Arguments TriJoinRecData' {A B C P} j1' j2' j3'. -Arguments Build_TriJoinRecData' {A B C P}%type_scope - (j1' j2' j3' j12' j13' j23' j123')%function_scope. +Arguments Build_TriJoinRecData' {A B C P}%_type_scope + (j1' j2' j3' j12' j13' j23' j123')%_function_scope. Definition prism' {P : Type} {a b c : P} {ab : a = b} {ac : a = c} {bc : b = c} (abc : ab @ bc = ac) diff --git a/theories/Homotopy/Suspension.v b/theories/Homotopy/Suspension.v index c515c9b11e8..ef8278d2286 100644 --- a/theories/Homotopy/Suspension.v +++ b/theories/Homotopy/Suspension.v @@ -75,7 +75,7 @@ Definition Susp_rec {X Y : Type} : Susp X -> Y := Pushout_rec (f:=const_tt X) (g:=const_tt X) Y (Unit_ind H_N) (Unit_ind H_S) H_merid. -Global Arguments Susp_rec {X Y}%type_scope H_N H_S H_merid%function_scope _. +Global Arguments Susp_rec {X Y}%_type_scope H_N H_S H_merid%_function_scope _. Definition Susp_rec_beta_merid {X Y : Type} {H_N H_S : Y} {H_merid : X -> H_N = H_S} (x:X) diff --git a/theories/Limits/Pullback.v b/theories/Limits/Pullback.v index eddd9dd7e44..d0e90b25233 100644 --- a/theories/Limits/Pullback.v +++ b/theories/Limits/Pullback.v @@ -11,7 +11,7 @@ Local Open Scope path_scope. Definition Pullback {A B C} (f : B -> A) (g : C -> A) := { b : B & { c : C & f b = g c }}. -Global Arguments Pullback {A B C}%type_scope (f g)%function_scope. +Global Arguments Pullback {A B C}%_type_scope (f g)%_function_scope. (** The universal commutative square *) Definition pullback_pr1 {A B C} {f : B -> A} {g : C -> A} diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v index 5c6bd70469f..72480c5ea88 100644 --- a/theories/Modalities/ReflectiveSubuniverse.v +++ b/theories/Modalities/ReflectiveSubuniverse.v @@ -241,12 +241,12 @@ Section ORecursion. End ORecursion. (* We never want to see [extendable_to_O]. The [!x] allows [cbn] to unfold these when passed a constructor, such as [tr x]. This, for example, means that [O_rec (O:=Tr n) f (tr x)] will compute to [f x] and [Trunc_functor n f (tr x)] will compute to [tr (f x)]. *) -Arguments O_rec {O} {P Q}%type_scope {Q_inO H H0} f%function_scope !x. -Arguments O_rec_beta {O} {P Q}%type_scope {Q_inO H H0} f%function_scope !x. -Arguments O_indpaths {O} {P Q}%type_scope {Q_inO H H0} (g h)%function_scope p !x. -Arguments O_indpaths_beta {O} {P Q}%type_scope {Q_inO H H0} (g h)%function_scope p !x. -Arguments O_ind2paths {O} {P Q}%type_scope {Q_inO H H0} {g h}%function_scope p q r !x. -Arguments O_ind2paths_beta {O} {P Q}%type_scope {Q_inO H H0} {g h}%function_scope p q r !x. +Arguments O_rec {O} {P Q}%_type_scope {Q_inO H H0} f%_function_scope !x. +Arguments O_rec_beta {O} {P Q}%_type_scope {Q_inO H H0} f%_function_scope !x. +Arguments O_indpaths {O} {P Q}%_type_scope {Q_inO H H0} (g h)%_function_scope p !x. +Arguments O_indpaths_beta {O} {P Q}%_type_scope {Q_inO H H0} (g h)%_function_scope p !x. +Arguments O_ind2paths {O} {P Q}%_type_scope {Q_inO H H0} {g h}%_function_scope p q r !x. +Arguments O_ind2paths_beta {O} {P Q}%_type_scope {Q_inO H H0} {g h}%_function_scope p q r !x. (** A tactic that generalizes [strip_truncations] to reflective subuniverses. [strip_truncations] introduces fewer universe variables, so tends to work better when removing truncations. [strip_modalities] in Modality.v also applies dependent elimination when [O] is a modality. *) Ltac strip_reflections := diff --git a/theories/Spaces/BinInt/Core.v b/theories/Spaces/BinInt/Core.v index 7f6f6f5e6b3..11f16d3fbf1 100644 --- a/theories/Spaces/BinInt/Core.v +++ b/theories/Spaces/BinInt/Core.v @@ -18,7 +18,7 @@ Inductive BinInt : Type0 := | zero : BinInt | pos : Pos -> BinInt. -Arguments pos p%pos. +Arguments pos p%_pos. Declare Scope binint_scope. Local Open Scope binint_scope. diff --git a/theories/Types/Forall.v b/theories/Types/Forall.v index 7cc510a17dc..e0dd105f7e6 100644 --- a/theories/Types/Forall.v +++ b/theories/Types/Forall.v @@ -50,7 +50,7 @@ Definition equiv_path_forall `{P : A -> Type} (f g : forall x, P x) : (f == g) <~> (f = g) := Build_Equiv _ _ (path_forall f g) _. -Global Arguments equiv_path_forall {A%type_scope P} (f g)%function_scope. +Global Arguments equiv_path_forall {A%_type_scope P} (f g)%_function_scope. (** ** Path algebra *) @@ -335,9 +335,9 @@ Global Instance isequiv_path_forall11 {A : Type} {B : A -> Type} `{P : forall a : IsEquiv (path_forall11 f g) | 0 := _. -Global Arguments equiv_path_forall11 {A B}%type_scope {P} (f g)%function_scope. +Global Arguments equiv_path_forall11 {A B}%_type_scope {P} (f g)%_function_scope. -Global Arguments path_forall11 {A B}%type_scope {P} (f g)%function_scope _. +Global Arguments path_forall11 {A B}%_type_scope {P} (f g)%_function_scope _. (** ** Truncatedness: any dependent product of n-types is an n-type: see [contr_forall] and [istrunc_forall] in Basics.Trunc. *) diff --git a/theories/Types/Universe.v b/theories/Types/Universe.v index 69e1c36a27b..5dac3f7b4b2 100644 --- a/theories/Types/Universe.v +++ b/theories/Types/Universe.v @@ -43,7 +43,7 @@ Definition path_universe_uncurried {A B : Type} (f : A <~> B) : A = B Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B) := path_universe_uncurried (Build_Equiv _ _ f feq). -Global Arguments path_universe {A B}%type_scope f%function_scope {feq}. +Global Arguments path_universe {A B}%_type_scope f%_function_scope {feq}. Definition eta_path_universe {A B : Type} (p : A = B) : path_universe (equiv_path A B p) = p diff --git a/theories/WildCat/Core.v b/theories/WildCat/Core.v index 7d250535bf3..bf917a67d9c 100644 --- a/theories/WildCat/Core.v +++ b/theories/WildCat/Core.v @@ -594,9 +594,9 @@ Record BasepointPreservingFunctor (B C : Type) bp_pointed : bp_map (point B) $-> point C }. -Arguments bp_pointed {B C}%type_scope {H H0 H1 H2 H3 H4} b. -Arguments Build_BasepointPreservingFunctor {B C}%type_scope {H H0 H1 H2 H3 H4} - bp_map%function_scope {bp_is0functor} bp_pointed. +Arguments bp_pointed {B C}%_type_scope {H H0 H1 H2 H3 H4} b. +Arguments Build_BasepointPreservingFunctor {B C}%_type_scope {H H0 H1 H2 H3 H4} + bp_map%_function_scope {bp_is0functor} bp_pointed. Coercion bp_map : BasepointPreservingFunctor >-> Funclass. diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v index b2ad2615de8..240906b2966 100644 --- a/theories/WildCat/Equiv.v +++ b/theories/WildCat/Equiv.v @@ -674,12 +674,12 @@ Class Cat_IsBiInv {A} `{Is1Cat A} {x y : A} (f : x $-> y) := { cat_eissect' : cat_equiv_inv' $o f $== Id x; }. -Arguments cat_equiv_inv {A}%type_scope { _ _ _ _ x y} f {_}. -Arguments cat_eisretr {A}%type_scope { _ _ _ _ x y} f {_}. -Arguments cat_equiv_inv' {A}%type_scope { _ _ _ _ x y} f {_}. -Arguments cat_eissect' {A}%type_scope { _ _ _ _ x y} f {_}. +Arguments cat_equiv_inv {A}%_type_scope { _ _ _ _ x y} f {_}. +Arguments cat_eisretr {A}%_type_scope { _ _ _ _ x y} f {_}. +Arguments cat_equiv_inv' {A}%_type_scope { _ _ _ _ x y} f {_}. +Arguments cat_eissect' {A}%_type_scope { _ _ _ _ x y} f {_}. -Arguments Build_Cat_IsBiInv {A}%type_scope {_ _ _ _ x y f} cat_equiv_inv cat_eisretr cat_equiv_inv' cat_eissect'. +Arguments Build_Cat_IsBiInv {A}%_type_scope {_ _ _ _ x y f} cat_equiv_inv cat_eisretr cat_equiv_inv' cat_eissect'. Record Cat_BiInv A `{Is1Cat A} (x y : A) := { cat_equiv_fun :> x $-> y;