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

src/Common.v

@@ -16,6 +16,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Global Set Implicit Arguments.
 Global Generalizable All Variables.
 Global Set Asymmetric Patterns.
+#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.
 
 Global Coercion is_true : bool >-> Sortclass.
 Coercion bool_of_sumbool {A B} (x : {A} + {B}) : bool := if x then true else false.

src/Common/BoundedLookup.v

@@ -3,6 +3,7 @@ Require Import Fiat.Common.ilist Fiat.Common.ilist2.
 
 From Stdlib Require Vector.
 Global Set Asymmetric Patterns.
+#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.
 
 (* Typeclasses for ensuring that a string is included
    in a list (i.e. a set of method names). This allows

src/Common/ReservedNotations.v

@@ -1,6 +1,7 @@
 (** Depend on the compatibility file, so when we switch versions of Coq, all the relevant notations files get rebuilt. *)
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Global Set Asymmetric Patterns.
+#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.
 
 Reserved Infix "∪" (at level 60, right associativity).
 Reserved Infix "∩" (at level 60, right associativity).

src/Common/Telescope/Core.v

@@ -1,6 +1,7 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 From Stdlib Require Import Relation_Definitions Morphisms.
 Global Set Asymmetric Patterns.
+#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.
 
 Module Export Telescope.
   Inductive Telescope := bottom | tele (A : Type) (B : A -> Telescope).

src/Common/Wf.v

@@ -9,6 +9,7 @@ Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Scheme Induction for Acc Sort Prop.
 Scheme Induction for Acc Sort Set.

src/FiniteSetADTs/WordInterface.v

@@ -5,6 +5,7 @@ Require Import Stdlib.Classes.Morphisms.
 
 Set Implicit Arguments.
 Global Set Asymmetric Patterns.
+#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.
 
 Module Type BedrockWordT.
   Axiom W : Type.

src/Parsers/StringLike/Core.v

@@ -8,6 +8,7 @@
 
 Global Set Keyed Unification. (* Makes [rewrite] faster in 8.5 / 8.6; we put it hear to not have to deal with compatibility issues in other files *)
 Global Set Asymmetric Patterns.
+#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.
 
 Set Implicit Arguments.
 Generalizable All Variables.
@@ -44,7 +45,7 @@
   Arguments StringLikeMin : clear implicits.
   Arguments StringLike Char {HSLM}.
   Arguments StringIso Char {HSLM}.
   Bind Scope string_like_scope with String.
   Delimit Scope string_like_scope with string_like.
   Infix "=s" := (@beq _ _ _) (at level 70, no associativity) : type_scope.
   Infix "=s" := (@bool_eq _ _ _) (at level 70, no associativity) : string_like_scope.

src/QueryStructure/Implementation/DataStructures/Bags/BagsInterface.v

@@ -3,6 +3,7 @@ Require Export Stdlib.Program.Program Stdlib.Sorting.Permutation.
 
 Unset Implicit Arguments.
 Global Set Asymmetric Patterns.
+#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.
 
 (* Enumerating the items of a Bag resulting from inserting
    an item [inserted] into a bag [container] is a permutation

src/QueryStructure/Specification/Representation/Notations.v

@@ -1,5 +1,6 @@
 Require Export Fiat.Common.Coq__8_4__8_5__Compat.
 Global Set Asymmetric Patterns.
+#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.
 
 Reserved Notation "t ! r"
          (no associativity, at level 2,