Adapt to rocq-prover/rocq#21849

Author: proux01

theories/ideas/DepDestruct.v

@@ -34,7 +34,7 @@ Declare Scope ITele_scope.
 Delimit Scope ITele_scope with IT.
 Bind Scope ITele_scope with ITele.
 Arguments iBase {_} _.
-Arguments iTele {_ _%type} _.
+Arguments iTele {_ _%_type} _.
 
 (** [ATele it] describes a applied version of the type described in
     [it]. For instance, if [it] represents the type [T] equals to
@@ -46,14 +46,14 @@ Arguments iTele {_ _%type} _.
 (* Delimit Scope ATele_scope with AT. *)
 (* Bind Scope ATele_scope with ATele. *)
 (* Arguments aBase {_ _}. *)
-(* Arguments aTele {_ _%type _} _%AT _. *)
+(* Arguments aTele {_ _%_type _} _%_AT _. *)
 
 Fixpoint ATele {sort} (it : ITele sort) : Type :=
   match it with
   | iBase T => unit
   | @iTele _ T f => { t : T & ATele (f t) }
   end.
-Arguments ATele {_} !_%IT : simpl nomatch.
+Arguments ATele {_} !_%_IT : simpl nomatch.
 Declare Scope ATele_scope.
 Delimit Scope ATele_scope with AT.
 Bind Scope ATele_scope with ATele.
@@ -67,7 +67,7 @@ Fixpoint ITele_App {isort} {it : ITele isort} : forall (args : ATele it), isort
   | iBase T => fun _ => T
   | iTele f => fun '(existT _ t a) => ITele_App a
   end.
-Arguments ITele_App {_ !_%IT} !_%AT : simpl nomatch.
+Arguments ITele_App {_ !_%_IT} !_%_AT : simpl nomatch.
 
 (** Represents a constructor of an inductive type. *)
 Inductive CTele {sort} (it : ITele sort) : Type :=
@@ -76,9 +76,9 @@ Inductive CTele {sort} (it : ITele sort) : Type :=
 Declare Scope CTele_scope.
 Delimit Scope CTele_scope with CT.
 Bind Scope CTele_scope with CTele.
-Arguments CTele {_} _%IT.
-Arguments cBase {_ _%IT} _%AT _.
-Arguments cProd {_ _%IT _%type} _.
+Arguments CTele {_} _%_IT.
+Arguments cBase {_ _%_IT} _%_AT _.
+Arguments cProd {_ _%_IT _%_type} _.
 
 
 (** Represents a constructor of an inductive type where all arguments are non-dependent *)
@@ -102,7 +102,7 @@ Fixpoint RTele {isort : Sort} (rsort : Sort) (it : ITele isort) : Type :=
   | iBase T => T -> rsort
   | iTele f => forall t, RTele rsort (f t)
   end.
-Arguments RTele {_} _ _%IT.
+Arguments RTele {_} _ _%_IT.
 
 Fixpoint RTele_App {isort rsort} {it : ITele isort} : forall (a : ATele it), RTele rsort it -> selem_of (ITele_App a) -> stype_of rsort :=
   match it as it' with

theories/ideas/Pre-typedtactics.v

@@ -136,7 +136,7 @@ Definition do_def n {A:Prop} (a:A) :=
 (* *)
 
 Definition myprod := prod.
-Arguments myprod _%type _%type.
+Arguments myprod _%_type _%_type.
 
 Notation "T1 '|m-' G" := (myprod T1 G)
   (at level 98, no associativity,

theories/ideas/SubgoalsStrict.v

@@ -31,7 +31,7 @@ Coercion n_to_g A n (nt : ntactic A n) : gtactic A := fun g=>pv <- nt g; M.ret p
     the composition of an ntactic with nth gtactics. *)
 Class NSeq (A B : Type) n (nt: ntactic A n) (l: mlist (gtactic B)) (pf: mlength l = n) :=
   nseq : gtactic B.
-Arguments nseq {A B _} _%tactic _%tactic _ {_}.
+Arguments nseq {A B _} _%_tactic _%_tactic _ {_}.
 
 Import Mtac2.lib.List.
 

theories/intf/M.v

@@ -375,7 +375,7 @@ Definition existing_instance (name : string) (priority : moption N) (global : bo
 Definition instantiate_evar {A : Type} {P : A -> Type} (e x : A) (succ : t (P x)) (fail : t (P e)) : t (P e).
   make. Qed.
 
-Arguments t _%type.
+Arguments t _%_type.
 
 Definition fmap {A:Type} {B:Type} (f : A -> B) (x : t A) : t B :=
   bind x (fun a => ret (f a)).

theories/lib/Specif.v

@@ -42,10 +42,10 @@ Inductive msigT2 (A:Type) (P Q:A -> Type) : Type :=
 
 (* Notations *)
 
-Arguments msig (A P)%type.
-Arguments msig2 (A P Q)%type.
-Arguments msigT (A P)%type.
-Arguments msigT2 (A P Q)%type.
+Arguments msig (A P)%_type.
+Arguments msig2 (A P Q)%_type.
+Arguments msigT (A P)%_type.
+Arguments msigT2 (A P Q)%_type.
 
 (* Notation "{ x  |  P }" := (msig (fun x => P)) : type_scope. *)
 (* Notation "{ x  |  P  & Q }" := (msig2 (fun x => P) (fun x => Q)) : type_scope. *)

theories/tactics/TacticsBase.v

@@ -299,7 +299,7 @@ Fixpoint gmap@{a b+} {A:Type@{a}} {B:Type@{b}} (tacs : mlist (gtactic A)) (gs :
 
 Class Seq (A B C : Type) : Prop :=
   seq : gtactic A -> C -> gtactic B.
-Arguments seq {A B C _} _%tactic _%tactic.
+Arguments seq {A B C _} _%_tactic _%_tactic.
 
 #[global] Instance seq_one@{a b+} {A:Type@{a}} {B:Type@{b}} : Seq A B (gtactic B) :=
   fun t1 t2 => bind t1 (fun _ => t2).

theories/tactics/Ttactics.v

@@ -53,7 +53,7 @@ Definition use {A} (t : tactic) : ttac A :=
     gs <- t g;
     let gs := dreduce (@mmap) (mmap (fun '(m: _, g) => g) gs) in
     M.ret (m: a, gs).
-Arguments use [_] _%tactic.
+Arguments use [_] _%_tactic.
 
 Definition idtac {A} : ttac A :=
     '(m: a, g) <- to_goal A;
@@ -69,7 +69,7 @@ Definition by' {A} (t : tactic) : ttac A :=
   | [m:] => ret (m: a, [m:])
   | _ => failwith "couldn't solve"
   end.
-Arguments by' [_] _%tactic.
+Arguments by' [_] _%_tactic.
 
 (** Coercion between an [M] program and a [ttac] *)
 Definition lift {A} (t : M A) : ttac A :=
@@ -364,7 +364,7 @@ Fixpoint match_goal_base (u : Unification)
 End MatchGoalTT.
 Import MatchGoalTT.
 
-Arguments match_goal_base _ _%TT.
+Arguments match_goal_base _ _%_TT.
 
 Module notations.
 (* Notation "[t: x | .. | y ]" := (TT.compi x (.. (TT.compi y (M.ret I)) ..)). *)