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

Kami/Decomposition.v

@@ -5,6 +5,7 @@ Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.Wf Kami.RefinementF
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section GivenLabelMap.
   Variable p: string -> (sigT SignT) -> option (sigT SignT).

Kami/Duplicate.v

@@ -8,6 +8,7 @@ Require Import Compare_dec.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section Duplicate.
   Variable m: nat -> Modules.

Kami/Ex/FifoCorrect.v

@@ -9,6 +9,7 @@ Import ListNotations.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Hint Unfold listIsEmpty listEnq listDeq listFirstElt: MethDefs.
 

Kami/Ex/InDepthTutorial.v

@@ -10,6 +10,7 @@ Import ListNotations.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Open Scope string.
 

Kami/Ext/BSyntax.v

@@ -4,6 +4,7 @@ Require Import Kami.Syntax Kami.Synthesize.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section VecFunc.
   Variables A B: Type.

Kami/Inline.v

@@ -5,6 +5,7 @@ Require Import Kami.Syntax.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section Base.
   Variable type: Kind -> Type.

Kami/InlineFacts.v

@@ -11,6 +11,7 @@ Require Import (hints) btauto.Algebra.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Ltac Tauto.intuition_solver ::= auto with datatypes exfalso.
 

Kami/Label.v

@@ -6,6 +6,7 @@ Import ListNotations.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** This file contains following definitions/facts about label manipulation.
  * - Lifting M.restrict and M.complement to the level of labels

Kami/Lib/Concat.v

@@ -2,6 +2,7 @@ From Coq Require Import List String.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Fixpoint concat A (ls: list (list A)): list A :=
   match ls with

Kami/Lib/FMap.v

@@ -12,6 +12,7 @@ Local Ltac Tauto.intuition_solver ::= auto with datatypes.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section Lists. (* For dealing with domains *)
   Context {A: Type}.

Kami/Lib/ListSupport.v

@@ -4,6 +4,7 @@ Import ListNotations.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Lemma Forall_app:
   forall {A} (l1 l2: list A) P, Forall P l1 -> Forall P l2 -> Forall P (l1 ++ l2).

Kami/Lib/Misc.v

@@ -3,6 +3,7 @@ Require Import StringAsList.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Theorem true_False_false: forall v, (v = true -> False) -> v = false.
 Proof.

Kami/Lib/Reflection.v

@@ -3,6 +3,7 @@ Require Import Lib.CommonTactics.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Fixpoint noDupStr (l: list string) :=
   match l with

Kami/Lib/StringAsList.v

@@ -1,6 +1,7 @@
 From Coq Require Import String Equality Lia.
 
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Open Scope string.
 

Kami/Lib/StringAsOT.v

@@ -2,6 +2,7 @@ From Coq Require Import PeanoNat Compare_dec Lia String Ascii.
 From Coq Require Import OrderedType.
 
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Lemma nat_compare_eq_refl : forall x, Nat.compare x x = Eq.
   intros; apply Nat.compare_eq_iff; trivial.

Kami/Lib/StringEq.v

@@ -2,6 +2,7 @@ From Coq Require Import Bool Ascii String List.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Definition ascii_eq (a1 a2: Ascii.ascii): bool :=
   match a1, a2 with

Kami/Lib/VectorFacts.v

@@ -3,6 +3,7 @@ Import Vector.VectorNotations.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Definition Vector_caseS'
            {A'} (Q : nat -> Type)

Kami/Lib/WordSupport.v

@@ -1,6 +1,7 @@
 Require Import Arith Lib.Word Lib.Nlia Lia.
 
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 Set Implicit Arguments.
 Local Open Scope word_scope.
 

Kami/Lib/ilist.v

@@ -2,6 +2,7 @@ Generalizable All Variables.
 Set Implicit Arguments.
 
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 From Coq Require Import List
         String

Kami/ModularFacts.v

@@ -4,6 +4,7 @@ Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.Wf.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Fixpoint composeLabels (ls1 ls2: LabelSeqT) :=
   match ls1, ls2 with

Kami/ModuleBound.v

@@ -5,6 +5,7 @@ Require Import Kami.Specialize Kami.Duplicate.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section ModuleBound.
   Variable m: Modules.

Kami/ModuleBoundEx.v

@@ -7,6 +7,7 @@ Import ListNotations.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section ModuleBound.
   Variable m: Modules.

Kami/Notations.v

@@ -4,6 +4,7 @@ Require Import Kami.Syntax.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** * Common notations for normal modules and meta-modules *)
 

Kami/PartialInlineFacts.v

@@ -11,6 +11,7 @@ Local Ltac Tauto.intuition_solver ::= auto with datatypes exfalso bool zarith.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Lemma notNamesNotIn: forall A l (x: Attribute A), ~ In (attrName x) (namesOf l) -> In x l -> False.
 Proof.

Kami/RefinementFacts.v

@@ -8,6 +8,7 @@ Import ListNotations.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Ltac Tauto.intuition_solver ::= auto with exfalso zarith.
 

Kami/Renaming.v

@@ -5,6 +5,7 @@ Require Import Lib.CommonTactics.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Ltac Tauto.intuition_solver ::= auto with datatypes.
 

Kami/SemFacts.v

@@ -5,6 +5,7 @@ Require Import Kami.Syntax Kami.Semantics Kami.Wf.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Ltac Tauto.intuition_solver ::= auto with exfalso datatypes.
 

Kami/Semantics.v

@@ -7,6 +7,7 @@ Require Import Kami.Syntax.
 Set Implicit Arguments.
 
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section VecFunc.
   Variable A: Type.

Kami/Specialize.v

@@ -7,6 +7,7 @@ From Coq Require Import Compare_dec.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Ltac Tauto.intuition_solver ::= auto with exfalso bool zarith.
 

Kami/StepDet.v

@@ -5,6 +5,7 @@ Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.Wf.
 Set Implicit Arguments.
 
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section NoCalls.
   Fixpoint actionNoCalls {retT} (a: ActionT typeUT retT) :=

Kami/Substitute.v

@@ -4,6 +4,7 @@ Require Import Kami.Syntax Kami.Semantics Kami.SemFacts Kami.RefinementFacts Kam
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section Interacting.
   Variables (regs regs' sregs oregs: list RegInitT).

Kami/Syntax.v

@@ -6,6 +6,7 @@ Require Import Eqdep. (* for signature_eq *)
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (* `Vec n` is effectively a map from bit vectors of length
    `n` to elements of `A` *)

Kami/Synthesize.v

@@ -3,6 +3,7 @@ Require Import Kami.Syntax Lib.Struct Kami.Notations.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Definition tyS: Kind -> Type := fun _ => nat.
 

Kami/Tactics.v

@@ -10,6 +10,7 @@ From Coq Require Import FunctionalExtensionality Equality.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (**
 - Kami Tactics

Kami/Tutorial.v

@@ -2,6 +2,7 @@ Require Import Kami.Kami.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** Welcome to the Kami tutorial!  This tutorial gives a demo of implementing and verifying very simple producer-consumer components. *)
 

Kami/Wf.v

@@ -6,6 +6,7 @@ From Coq Require Import FunctionalExtensionality Equality Eqdep Eqdep_dec.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Ltac Tauto.intuition_solver ::= auto with datatypes.