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

theories/Data/Checked.v

@@ -1,6 +1,7 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Section checked.
   Context {T : Type}.
@@ -35,4 +36,4 @@
       | Failure => None
     end.
 
-End checked.
+End checked.

theories/Data/Fin.v

@@ -7,6 +7,7 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 (** `fin n` corresponds to "naturals less than `n`",
     i.e. a finite set of size n

theories/Data/HList.v

@@ -11,6 +11,7 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 Set Universe Polymorphism.
 Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.

theories/Data/Member.v

@@ -11,6 +11,7 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Section member.
   Context {T : Type}.

theories/Data/Tuple.v

@@ -3,6 +3,7 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Fixpoint vector (T : Type) (n : nat) : Type :=
   match n with

theories/Data/Vector.v

@@ -3,6 +3,7 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Inductive vector T : nat -> Type :=
 | Vnil : vector T 0

theories/Programming/With.v

@@ -1,6 +1,7 @@
 Require Import Coq.Lists.List.
 
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Fixpoint Ctor {T : Type} (ls : list {x : Type & T -> x}) : Type :=
   match ls with
@@ -56,7 +57,7 @@
   (_strt : Struct T) (_acc : Accessor f) :=
   @structWith _ _ t _ v acc.
 
 Delimit Scope struct_scope with record.
 
 Notation "{$ x 'with' y ':=' v $}" := (@wrapWith _ _ x y v _ _) : struct_scope.
 

theories/Relations/TransitiveClosure.v

@@ -4,6 +4,7 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Section parametric.
   Variable T : Type.