Adapt to rocq-prover/rocq#21947

Author: proux01

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 @@ Section checked.
       | Failure => None
     end.
 
-End checked.
+End checked.

theories/Data/Fin.v

@@ -7,6 +7,7 @@ Require Import ExtLib.Tactics.Injection.
 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 @@ Require Import Coq.Classes.Morphisms.
 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 @@ Require Import ExtLib.Tactics.EqDep.
 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 @@ Require Import ExtLib.Data.Fin.
 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 @@ Require Import ExtLib.Data.Fin.
 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

theories/Relations/TransitiveClosure.v

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