[8.19] fix % in Arguments warnings

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.

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. *)
 

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)

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.

theories/Basics/Overture.v

@@ -2,7 +2,7 @@
 
 (** * Basic definitions of homotopy type theory, particularly the groupoid structure of identity types. *)
 (** Import the file of reserved notations so we maintain consistent level notations throughout the library *)
 Require Export Basics.Settings Basics.Notations.
 
 Local Set Polymorphic Inductive Cumulativity.
 
@@ -172,11 +172,11 @@
 
 (** 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 @@
 (** 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 @@
   := 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 @@
 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 @@
 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 @@
   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 @@
   : 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 @@
   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 @@
   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 @@
   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 @@
 
 (** 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 @@
   :=
   (@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 @@
 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 @@
 
 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.

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. *)

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.

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.

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. *)

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.

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.
 

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.*)

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.

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}

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)

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)

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)

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}