Adapt to https://github.com/rocq-prover/rocq/pull/21849

theories/Torch/Tensor.v

@@ -1230,7 +1230,7 @@ Definition arange {start : with_default "start" int 0%uint63} (stop : int) {step
   := fun idx => let idx := RawIndex.item idx in
                 (start + idx * step)%uint63.
 
-#[global] Arguments arange (_ _ _)%uint63.
+#[global] Arguments arange (_ _ _)%_uint63.
 #[global] Arguments arange {_} _ {_}, _ _ {_}, _ _ _.
 
 (* TODO: nary *)
@@ -1309,7 +1309,7 @@ Definition tril {rnk} {s : Shape rnk} {r c} {A} {zero : has_zero A}
      => if ((0 ≤? i) && (i <? r) && (Sint63.max 0 (1 + i + diagonal) ≤? j) && (j <? c))%bool
         then 0%core
         else input idxs.
-#[global] Arguments tril {rnk%nat s%shape} {r c}%uint63 {A%type_scope zero} {diagonal}%sint63 input%tensor.
+#[global] Arguments tril {rnk%_nat s%_shape} {r c}%_uint63 {A%_type_scope zero} {diagonal}%_sint63 input%_tensor.
 (** Quoting https://pytorch.org/docs/stable/generated/torch.triu.html
 
 torch.triu(input, diagonal=0, *, out=None) → Tensor
@@ -1335,7 +1335,7 @@ Definition triu {rnk} {s : Shape rnk} {r c} {A} {zero : has_zero A}
      => if ((0 ≤? i) && (i <? r) && (0 ≤? j) && (j <? Sint63.max 0 (i + diagonal)))%bool
         then 0%core
         else input idxs.
-#[global] Arguments triu {rnk%nat s%shape} {r c}%uint63 {A%type_scope zero} {diagonal}%sint63 input%tensor.
+#[global] Arguments triu {rnk%_nat s%_shape} {r c}%_uint63 {A%_type_scope zero} {diagonal}%_sint63 input%_tensor.
 
 (** Quoting
 https://pytorch.org/docs/stable/generated/torch.diagonal.html
@@ -1365,7 +1365,7 @@ Definition diagonal {b} {s : Shape b} {r c} {A}
           => input ((idxs, i - offset), i)%uint63
      else fun '(idxs, i)
           => input ((idxs, i), i + offset)%uint63.
-#[global] Arguments diagonal {b%nat s%shape} {r c}%uint63 {A%type_scope} {offset}%sint63 input%tensor.
+#[global] Arguments diagonal {b%_nat s%_shape} {r c}%_uint63 {A%_type_scope} {offset}%_sint63 input%_tensor.
 
 Definition coer_tensor {r s A B} {coerAB : has_coer A B} : @tensor r s A -> @tensor r s B
   := Tensor.map coer.

theories/Util/Classes/Morphisms/Dependent.v

@@ -216,20 +216,20 @@ Notation const6 R := (match _ as F return forall A B, Hetero.relation A B -> for
                       | F => fun (A B : Type) (_ : Hetero.relation A B) (A' B' : Type) (_ : Hetero.relation A' B') (A'' B'' : Type) (_ : Hetero.relation A'' B'') (A''' B''' : Type) (_ : Hetero.relation A''' B''') (A'''' B'''' : Type) (_ : Hetero.relation A'''' B'''') (A''''' B''''' : Type) (_ : Hetero.relation A''''' B''''') => R
                       end) (only parsing).
 Notation constR6 R := (fun (A B : Type) (_ : Hetero.relation A B) (A' B' : Type) (_ : Hetero.relation A' B') (A'' B'' : Type) (_ : Hetero.relation A'' B'') (A''' B''' : Type) (_ : Hetero.relation A''' B''') (A'''' B'''' : Type) (_ : Hetero.relation A'''' B'''') (A''''' B''''' : Type) (_ : Hetero.relation A''''' B''''') => R).
-Arguments Proper {F}%type R%dependent_signature m.
-Arguments respectful {A B}%type (R R')%dependent_signature (_ _)%type _ _.
-Arguments Proper2 {F}%type R%dependent2_signature m.
-Arguments respectful2 {A B}%type (R R')%dependent2_signature (_ _)%type _ _.
-Arguments Proper3 {F}%type R%dependent3_signature m.
-Arguments respectful3 {A B}%type (R R')%dependent3_signature (_ _)%type _ _.
-Arguments Proper4 {F}%type R%dependent4_signature m.
-Arguments respectful4 {A B}%type (R R')%dependent4_signature (_ _)%type _ _.
-Arguments Proper5 {F}%type R%dependent5_signature m.
-Arguments respectful5 {A B}%type (R R')%dependent5_signature (_ _)%type _ _.
-Arguments Proper6 {F}%type R%dependent6_signature m.
-Arguments respectful6 {A B}%type (R R')%dependent6_signature (_ _)%type _ _.
-Arguments Propern {n}%nat {F}%type R%dependentn_signature m.
-Arguments respectfuln {n}%nat {A B}%type (R R')%dependentn_signature.
+Arguments Proper {F}%_type R%_dependent_signature m.
+Arguments respectful {A B}%_type (R R')%_dependent_signature (_ _)%_type _ _.
+Arguments Proper2 {F}%_type R%_dependent2_signature m.
+Arguments respectful2 {A B}%_type (R R')%_dependent2_signature (_ _)%_type _ _.
+Arguments Proper3 {F}%_type R%_dependent3_signature m.
+Arguments respectful3 {A B}%_type (R R')%_dependent3_signature (_ _)%_type _ _.
+Arguments Proper4 {F}%_type R%_dependent4_signature m.
+Arguments respectful4 {A B}%_type (R R')%_dependent4_signature (_ _)%_type _ _.
+Arguments Proper5 {F}%_type R%_dependent5_signature m.
+Arguments respectful5 {A B}%_type (R R')%_dependent5_signature (_ _)%_type _ _.
+Arguments Proper6 {F}%_type R%_dependent6_signature m.
+Arguments respectful6 {A B}%_type (R R')%_dependent6_signature (_ _)%_type _ _.
+Arguments Propern {n}%_nat {F}%_type R%_dependentn_signature m.
+Arguments respectfuln {n}%_nat {A B}%_type (R R')%_dependentn_signature.
 
 Local Open Scope dependent_signature_scope.
 
@@ -298,8 +298,8 @@ Section Relations.
 End Relations.
 
 Global Typeclasses Opaque respectful pointwise_relation forall_relation.
-Arguments forall_relation {A P}%type sig%signature _ _.
-Arguments pointwise_relation A%type {B}%type R%signature _ _.
+Arguments forall_relation {A P}%_type sig%_signature _ _.
+Arguments pointwise_relation A%_type {B}%_type R%_signature _ _.
 
 #[global]
 Hint Unfold Reflexive : core.

theories/Util/PArray.v

@@ -161,7 +161,7 @@
          }}.
 
 Export SliceNotations.
 Notation "x .[ < s > ]" := (slice x s) (s custom slice at level 60, format "x .[ < s > ]") : core_scope.
 
 Definition repeat {A} (xs : A) (count : int) : array A
   := PArray.make count xs.
@@ -203,7 +203,7 @@
            in
            set (out.[i <- row])
        }}.
-#[global] Arguments tril {A%type_scope zero diagonal%sint63} input.
+#[global] Arguments tril {A%_type_scope zero diagonal%_sint63} input.
 
 (** Quoting https://pytorch.org/docs/stable/generated/torch.triu.html
 
@@ -239,4 +239,4 @@
            in
            set (out.[i <- row])
        }}.
-#[global] Arguments triu {A%type_scope zero diagonal%sint63} input.
+#[global] Arguments triu {A%_type_scope zero diagonal%_sint63} input.

theories/Util/PolymorphicSigma.v

@@ -21,10 +21,10 @@
 
 (* Notations *)
 
-Arguments sig (A P)%type.
-Arguments sig2 (A P Q)%type.
-Arguments sigT (A P)%type.
-Arguments sigT2 (A P Q)%type.
+Arguments sig (A P)%_type.
+Arguments sig2 (A P Q)%_type.
+Arguments sigT (A P)%_type.
+Arguments sigT2 (A P Q)%_type.
 
 Module Import Notations.
   #[export] Set Warnings "-notation-overridden".