Adapt to rocq-prover/rocq#21849

Author: proux01

src/ArithmeticCPS/Core.v

@@ -48,12 +48,12 @@ Module Type Runtime.
   Parameter runtime_div : Z -> Z -> Z.
   Parameter runtime_modulo : Z -> Z -> Z.
   Parameter runtime_opp : Z -> Z.
-  Arguments runtime_add (_ _)%RT.
-  Arguments runtime_sub (_ _)%RT.
-  Arguments runtime_mul (_ _)%RT.
-  Arguments runtime_div _%RT _%Z.
-  Arguments runtime_modulo _%RT _%Z.
-  Arguments runtime_opp _%RT.
+  Arguments runtime_add (_ _)%_RT.
+  Arguments runtime_sub (_ _)%_RT.
+  Arguments runtime_mul (_ _)%_RT.
+  Arguments runtime_div _%_RT _%_Z.
+  Arguments runtime_modulo _%_RT _%_Z.
+  Arguments runtime_opp _%_RT.
   Infix "*" := runtime_mul : runtime_scope.
   Infix "+" := runtime_add : runtime_scope.
   Infix "-" := runtime_sub : runtime_scope.

src/BoundsPipeline.v

@@ -421,7 +421,7 @@ Module Pipeline.
           | Success x => k x
           | Error err => Debug.ret (Error err)
           end)%debugM.
-    Global Arguments bind {A B}%type_scope (x k)%pipelineM_scope.
+    Global Arguments bind {A B}%_type_scope (x k)%_pipelineM_scope.
     Notation sequence x y := (@bind unit _ x%pipelineM (fun 'tt => y%pipelineM)).
     Notation ret x := (@Debug.ret string _ (@Success ErrorMessage _ x)).
     Notation err msg := (@Debug.ret string _ (@Error ErrorMessage _ msg)).

src/Language/APINotations.v

@@ -379,7 +379,7 @@ Module Compilers.
       Delimit Scope ident_scope with ident.
       Bind Scope ident_scope with ident.
       Notation interp := Compilers.ident_interp (only parsing).
-      Global Arguments expr.Ident {base_type%type ident%function var%function t%etype} idc%ident.
+      Global Arguments expr.Ident {base_type%_type ident%_function var%_function t%_etype} idc%_ident.
       Notation "## x" := (Compilers.ident_Literal x) (only printing) : ident_scope.
       Notation "## x" := (Compilers.ident_Literal (t:=base.reify_base_type_of x) x) (only parsing) : ident_scope.
       Notation "## x" := (expr.Ident (Compilers.ident_Literal x)) (only printing) : expr_scope.

src/Util/Decidable.v

@@ -11,7 +11,7 @@ From Coq Require Import BinNat.
 Local Open Scope type_scope.
 
 Class Decidable (P : Prop) := dec : {P} + {~P}.
-Arguments dec _%type_scope {_}.
+Arguments dec _%_type_scope {_}.
 Notation DecidableRel R := (forall x y, Decidable (R x y)).
 
 Global Instance hprop_eq_dec {A} `{DecidableRel (@eq A)} : IsHPropRel (@eq A) | 10.

src/Util/PointedProp.v

@@ -56,14 +56,14 @@ Definition not_option_pointed_Prop (x : option pointed_Prop) : option pointed_Pr
      | None => Some trivial
      | Some (inject p) => Some (inject (~p))
      end.
-Arguments not_option_pointed_Prop _%option_pointed_prop.
+Arguments not_option_pointed_Prop _%_option_pointed_prop.
 
 Definition and_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop
   := match x, y with
      | Some x, Some y => Some (and_pointed_Prop x y)
      | _, _ => None
      end.
-Arguments and_option_pointed_Prop (_ _)%option_pointed_prop.
+Arguments and_option_pointed_Prop (_ _)%_option_pointed_prop.
 
 Definition or_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop
   := match x, y with
@@ -72,15 +72,15 @@ Definition or_option_pointed_Prop (x y : option pointed_Prop) : option pointed_P
      | None, Some y => Some y
      | None, None => None
      end.
-Arguments or_option_pointed_Prop (_ _)%option_pointed_prop.
+Arguments or_option_pointed_Prop (_ _)%_option_pointed_prop.
 
 Definition impl_option_pointed_Prop (x y : option pointed_Prop) : option pointed_Prop
   := match x, y with
      | None, _ => Some trivial
      | Some x, Some y => Some (impl_pointed_Prop x y)
      | Some p, None => not_option_pointed_Prop p
      end.
-Arguments impl_option_pointed_Prop (_ _)%option_pointed_prop.
+Arguments impl_option_pointed_Prop (_ _)%_option_pointed_prop.
 
 Infix "/\" := and_pointed_Prop : pointed_prop_scope.
 Infix "\/" := or_pointed_Prop : pointed_prop_scope.

src/Util/Wf1.v

@@ -373,8 +373,8 @@ for fixn in range(1, 11):
   Definition Fix%(fixn)d_Proper_eq_with_assumption : Fix%(fixn)d_Proper_eq_with_assumption'T := Fix%(fixn)d_Proper_eq_with_assumption'.
 End Fix%(fixn)d.
 
-Arguments Fix%(fixn)d_Proper_eq {%(letters)s R Rwf P} %(fix_underscores)s.
-Arguments Fix%(fixn)d_Proper_eq_with_assumption {%(letters)s R Rwf P} _ _ %(fix_underscores)s.
+Arguments Fix%_(fixn)d_Proper_eq {%_(letters)s R Rwf P} %_(fix_underscores)s.
+Arguments Fix%_(fixn)d_Proper_eq_with_assumption {%_(letters)s R Rwf P} _ _ %_(fix_underscores)s.
 Global Existing Instance Fix%(fixn)d_Proper_eq.
 Global Existing Instance Fix%(fixn)d_Proper_eq_with_assumption.
 """ % locals())

src/Util/Wf2.v

@@ -576,8 +576,8 @@ for fixn in range(1, 11):
   Definition Fix%(fixn)d_2_%(fixn)d_eq : Fix%(fixn)d_2_%(fixn)d_eq'T := Fix%(fixn)d_2_%(fixn)d_eq'.
 End Fix2_%(fixn)d.
 
-Arguments Fix2_%(fixn)d_Proper_eq {A A' %(letters)s R Rwf P} %(fix_underscores)s.
-Arguments Fix2_%(fixn)d_Proper_eq_with_assumption {A A' %(letters)s R Rwf P} _ _ %(fix_underscores)s.
+Arguments Fix2_%_(fixn)d_Proper_eq {A A' %_(letters)s R Rwf P} %_(fix_underscores)s.
+Arguments Fix2_%_(fixn)d_Proper_eq_with_assumption {A A' %_(letters)s R Rwf P} _ _ %_(fix_underscores)s.
 Global Existing Instance Fix2_%(fixn)d_Proper_eq.
 Global Existing Instance Fix2_%(fixn)d_Proper_eq_with_assumption.
 """ % locals())