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

finmap.v

@@ -148,10 +148,10 @@
 Reserved Notation "A `=P` B" (at level 70, no associativity).
 
 Reserved Notation "f @`[ key ] A" (at level 24, key at level 0).
 Reserved Notation "f @2`[ key ] ( A , B )"
   (at level 24, format "f  @2`[ key ]  ( A ,  B )").
 Reserved Notation "f @` A" (at level 24).
 Reserved Notation "f @2` ( A , B )" (at level 24, format "f  @2`  ( A ,  B )").
 
 (* unary *)
 Reserved Notation "[ 'fset' E | x : T 'in' A ]" (at level 0, E, x at level 99).
@@ -169,9 +169,9 @@
 Reserved Notation "[ 'fset' x 'in' A | P & Q ]" (at level 0, x at level 99).
 
 (* binary *)
 Reserved Notation "[ 'fset' E | x : T 'in' A , y : T' 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset' E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 
 (* keyed parse only *)
@@ -184,11 +184,11 @@
   (at level 0, E, x at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A & P ]"
   (at level 0, E, x at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : T 'in' A , y : T' 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A , y : B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99).
 Reserved Notation "[ 'fset[' key ] E | x : A , y 'in' B ]"
   (at level 0, E, x, y at level 99).
@@ -234,7 +234,7 @@
 Reserved Notation "[ 'f' 'set' x 'in' A | P & Q ]"
   (at level 0, x at level 99, format "[ 'f' 'set'  x  'in'  A  |  P  &  Q ]").
 (* binary printing only *)
 Reserved Notation "[ 'f' 'set' E | x 'in' A , y 'in' B ]"
   (at level 0, E, x at level 99, A at level 200, y at level 99,
    format "[ '[hv' 'f' 'set'  E '/ '  |  x  'in'  A , '/' y  'in'  B ] ']'").
 
@@ -358,7 +358,7 @@
 Defined.
 Arguments PredType [T pT] toP.
 
 Local Notation predOfType T := (pred_of_simpl (@pred_of_argType T)).
 
 Definition oextract (T : Type) (o : option T) : o -> T :=
   if o is Some t return o -> T then fun=> t else False_rect T \o notF.
@@ -403,7 +403,7 @@
 Implicit Types (k : K) (ks : seq K).
 Definition f (s : seq K) := choose (perm_eq (undup s)) (undup s).
 Fact perm s : perm_eq (f s) (undup s).
 Proof. by rewrite perm_sym chooseP. Qed.
 Fact uniq s : uniq (f s).
 Proof. by rewrite (perm_uniq (perm _)) undup_uniq. Qed.
 Fact E (s : seq K) : f s =i s.
@@ -485,7 +485,7 @@
 
 End Def.
 
-Arguments finSet K%type_scope.
+Arguments finSet K%_type_scope.
 
 #[warning="-deprecated-reference"]
 Identity Coercion type_of_finset : finset_of >-> finSet.
@@ -2977,7 +2977,7 @@
 
 End DefMap.
 
-Arguments finMap K%type_scope V%type_scope.
+Arguments finMap K%_type_scope V%_type_scope.
 
 Notation "{ 'fmap' K -> T }" := (finMap K T) : type_scope.