Merge pull request #171 from proux01/rocq21849

Adapt to rocq-prover/rocq#21849

Author: jwiegley

Adjunction/Hom.v

@@ -279,4 +279,4 @@ Qed.
 
 End AdjunctionHom.
 
-Arguments Adjunction_Hom {C D} F%functor U%functor.
+Arguments Adjunction_Hom {C D} F%_functor U%_functor.

Adjunction/Natural/Transformation.v

@@ -24,7 +24,7 @@ Class Adjunction_Transform := {
 
 End AdjunctionTransform.
 
-Arguments Adjunction_Transform {C D} F%functor U%functor.
+Arguments Adjunction_Transform {C D} F%_functor U%_functor.
 
 Declare Scope adjunction_scope.
 Declare Scope adjunction_type_scope.

Structure/End.v

@@ -14,8 +14,8 @@ Class End `(F : C^op ∏ C ⟶ D) := {
     wedge_map[end_wedge] ∘ u ≈ @wedge_map _ _ _ W x
 }.
 
-Arguments End {_%category _%category} F%functor.
-Arguments end_wedge {_%category _%category} F%functor {_}.
+Arguments End {_%_category _%_category} F%_functor.
+Arguments end_wedge {_%_category _%_category} F%_functor {_}.
 
 Coercion wedge_obj `(F : C^op ∏ C ⟶ D) (E : End F) := @end_wedge _ _ _ E.
 

Structure/Pullback/Limit.v

@@ -12,10 +12,10 @@ Require Import Category.Instance.Roof.
 Generalizable All Variables.
 
 Definition Pullback_Limit {C : Category} (F : Cospan C) := Limit F.
-Arguments Pullback_Limit {_%category} F%functor /.
+Arguments Pullback_Limit {_%_category} F%_functor /.
 
 Definition Pushout_Limit {C : Category} (F : Span C) := Colimit F.
-Arguments Pushout_Limit {_%category} F%functor /.
+Arguments Pushout_Limit {_%_category} F%_functor /.
 
 Program Definition Pullback_to_Universal {C : Category}
         (F : Cospan C) (P : Pullback_Limit F) :

Theory/Adjunction.v

@@ -248,7 +248,7 @@ Proof. intros; now rewrites. Qed.
 
 End Adjunction.
 
-Arguments Adjunction {C D} F%functor U%functor.
+Arguments Adjunction {C D} F%_functor U%_functor.
 
 Declare Scope adjunction_scope.
 Declare Scope adjunction_type_scope.

Theory/Category.v

@@ -67,8 +67,8 @@ Delimit Scope object_scope with object.
 Delimit Scope homset_scope with homset.
 Delimit Scope morphism_scope with morphism.
 
-Arguments dom {_%category _%object _%object} _%morphism.
-Arguments cod {_%category _%object _%object} _%morphism.
+Arguments dom {_%_category _%_object _%_object} _%_morphism.
+Arguments cod {_%_category _%_object _%_object} _%_morphism.
 
 Notation "obj[ C ]" := (@obj C%category)
   (at level 0, format "obj[ C ]") : type_scope.
@@ -178,12 +178,12 @@ Proof. split; auto. Qed.
 
 End Category.
 
-Arguments dom {_%category _%object _%object} _%morphism.
-Arguments cod {_%category _%object _%object} _%morphism.
-Arguments id_left {_%category _%object _%object} _%morphism.
-Arguments id_right {_%category _%object _%object} _%morphism.
-Arguments comp_assoc {_%category _%object _%object _%object _%object}
-  _%morphism _%morphism _%morphism.
+Arguments dom {_%_category _%_object _%_object} _%_morphism.
+Arguments cod {_%_category _%_object _%_object} _%_morphism.
+Arguments id_left {_%_category _%_object _%_object} _%_morphism.
+Arguments id_right {_%_category _%_object _%_object} _%_morphism.
+Arguments comp_assoc {_%_category _%_object _%_object _%_object _%_object}
+  _%_morphism _%_morphism _%_morphism.
 
 #[export]
 Program Instance hom_preorder {C : Category} : PreOrder (@hom C) := {

Theory/Functor.v

@@ -45,7 +45,7 @@ Notation "C ⟶ D" := (@Functor C%category D%category)
   (at level 90, right associativity) : functor_type_scope.
 
 Arguments fmap
-  {C%category D%category Functor%functor x%object y%object} f%morphism.
+  {C%_category D%_category Functor%_functor x%_object y%_object} f%_morphism.
 
 Infix "<$>" := fmap
   (at level 29, left associativity, only parsing) : morphism_scope.

Theory/Isomorphism.v

@@ -144,8 +144,8 @@ Notation "x ≅ y" := (@Isomorphism _%category x%object y%object)
 Notation "x ≅[ C ] y" := (@Isomorphism C%category x%object y%object)
   (at level 91, only parsing) : isomorphism_scope.
 
-Arguments to {_%category x%object y%object} _%morphism.
-Arguments from {_%category x%object y%object} _%morphism.
+Arguments to {_%_category x%_object y%_object} _%_morphism.
+Arguments from {_%_category x%_object y%_object} _%_morphism.
 Arguments iso_to_from {_ _ _} _.
 Arguments iso_from_to {_ _ _} _.