From c1716ebd9515784de76f04e7afef1790a7642096 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 23 Apr 2026 13:06:20 +0200
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21947

---
 Kami/Decomposition.v      | 1 +
 Kami/Duplicate.v          | 1 +
 Kami/Ex/FifoCorrect.v     | 1 +
 Kami/Ex/InDepthTutorial.v | 1 +
 Kami/Ext/BSyntax.v        | 1 +
 Kami/Inline.v             | 1 +
 Kami/InlineFacts.v        | 1 +
 Kami/Label.v              | 1 +
 Kami/Lib/Concat.v         | 1 +
 Kami/Lib/FMap.v           | 1 +
 Kami/Lib/ListSupport.v    | 1 +
 Kami/Lib/Misc.v           | 1 +
 Kami/Lib/Reflection.v     | 1 +
 Kami/Lib/StringAsList.v   | 1 +
 Kami/Lib/StringAsOT.v     | 1 +
 Kami/Lib/StringEq.v       | 1 +
 Kami/Lib/VectorFacts.v    | 1 +
 Kami/Lib/WordSupport.v    | 1 +
 Kami/Lib/ilist.v          | 1 +
 Kami/ModularFacts.v       | 1 +
 Kami/ModuleBound.v        | 1 +
 Kami/ModuleBoundEx.v      | 1 +
 Kami/Notations.v          | 1 +
 Kami/PartialInlineFacts.v | 1 +
 Kami/RefinementFacts.v    | 1 +
 Kami/Renaming.v           | 1 +
 Kami/SemFacts.v           | 1 +
 Kami/Semantics.v          | 1 +
 Kami/Specialize.v         | 1 +
 Kami/StepDet.v            | 1 +
 Kami/Substitute.v         | 1 +
 Kami/Syntax.v             | 1 +
 Kami/Synthesize.v         | 1 +
 Kami/Tactics.v            | 1 +
 Kami/Tutorial.v           | 1 +
 Kami/Wf.v                 | 1 +
 36 files changed, 36 insertions(+)

diff --git a/Kami/Decomposition.v b/Kami/Decomposition.v
index 4871fc28..ef9cb758 100644
--- a/Kami/Decomposition.v
+++ b/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).
diff --git a/Kami/Duplicate.v b/Kami/Duplicate.v
index 0cde3f7d..3a75ccb6 100644
--- a/Kami/Duplicate.v
+++ b/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.
diff --git a/Kami/Ex/FifoCorrect.v b/Kami/Ex/FifoCorrect.v
index 3d49fca4..da2c3168 100644
--- a/Kami/Ex/FifoCorrect.v
+++ b/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.
 
diff --git a/Kami/Ex/InDepthTutorial.v b/Kami/Ex/InDepthTutorial.v
index 48a55e8a..739b8d25 100644
--- a/Kami/Ex/InDepthTutorial.v
+++ b/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.
 
diff --git a/Kami/Ext/BSyntax.v b/Kami/Ext/BSyntax.v
index 13c2362a..fcd0724b 100644
--- a/Kami/Ext/BSyntax.v
+++ b/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.
diff --git a/Kami/Inline.v b/Kami/Inline.v
index e0a60489..0fb3689a 100644
--- a/Kami/Inline.v
+++ b/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.
diff --git a/Kami/InlineFacts.v b/Kami/InlineFacts.v
index 458cd99f..d195bc85 100644
--- a/Kami/InlineFacts.v
+++ b/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.
 
diff --git a/Kami/Label.v b/Kami/Label.v
index 9b857193..1d0e3cdc 100644
--- a/Kami/Label.v
+++ b/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
diff --git a/Kami/Lib/Concat.v b/Kami/Lib/Concat.v
index 74564640..f6191448 100644
--- a/Kami/Lib/Concat.v
+++ b/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
diff --git a/Kami/Lib/FMap.v b/Kami/Lib/FMap.v
index b56f8335..b3215e10 100644
--- a/Kami/Lib/FMap.v
+++ b/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}.
diff --git a/Kami/Lib/ListSupport.v b/Kami/Lib/ListSupport.v
index 2615b665..2db591a5 100644
--- a/Kami/Lib/ListSupport.v
+++ b/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).
diff --git a/Kami/Lib/Misc.v b/Kami/Lib/Misc.v
index c8da272b..d3e89625 100644
--- a/Kami/Lib/Misc.v
+++ b/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.
diff --git a/Kami/Lib/Reflection.v b/Kami/Lib/Reflection.v
index 51b30034..d26c9715 100644
--- a/Kami/Lib/Reflection.v
+++ b/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
diff --git a/Kami/Lib/StringAsList.v b/Kami/Lib/StringAsList.v
index 846392c1..7e5a3155 100644
--- a/Kami/Lib/StringAsList.v
+++ b/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.
 
diff --git a/Kami/Lib/StringAsOT.v b/Kami/Lib/StringAsOT.v
index daa0ec62..25a2b449 100644
--- a/Kami/Lib/StringAsOT.v
+++ b/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.
diff --git a/Kami/Lib/StringEq.v b/Kami/Lib/StringEq.v
index 09374555..c193f84f 100644
--- a/Kami/Lib/StringEq.v
+++ b/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
diff --git a/Kami/Lib/VectorFacts.v b/Kami/Lib/VectorFacts.v
index 694b6cd7..af42c217 100644
--- a/Kami/Lib/VectorFacts.v
+++ b/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)
diff --git a/Kami/Lib/WordSupport.v b/Kami/Lib/WordSupport.v
index 6a4b8034..b5062431 100644
--- a/Kami/Lib/WordSupport.v
+++ b/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.
 
diff --git a/Kami/Lib/ilist.v b/Kami/Lib/ilist.v
index f3d41f6d..6dd09746 100644
--- a/Kami/Lib/ilist.v
+++ b/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
diff --git a/Kami/ModularFacts.v b/Kami/ModularFacts.v
index f6b941c4..c150e91d 100644
--- a/Kami/ModularFacts.v
+++ b/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
diff --git a/Kami/ModuleBound.v b/Kami/ModuleBound.v
index c803593f..b715c0fe 100644
--- a/Kami/ModuleBound.v
+++ b/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.
diff --git a/Kami/ModuleBoundEx.v b/Kami/ModuleBoundEx.v
index 58073c9c..3f4d55e5 100644
--- a/Kami/ModuleBoundEx.v
+++ b/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.
diff --git a/Kami/Notations.v b/Kami/Notations.v
index bf86a914..1f350c6e 100644
--- a/Kami/Notations.v
+++ b/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 *)
 
diff --git a/Kami/PartialInlineFacts.v b/Kami/PartialInlineFacts.v
index 225d7a62..e8e1d36c 100644
--- a/Kami/PartialInlineFacts.v
+++ b/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.
diff --git a/Kami/RefinementFacts.v b/Kami/RefinementFacts.v
index 79ae6bf5..68c7b49a 100644
--- a/Kami/RefinementFacts.v
+++ b/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.
 
diff --git a/Kami/Renaming.v b/Kami/Renaming.v
index 822008c8..674d732a 100644
--- a/Kami/Renaming.v
+++ b/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.
 
diff --git a/Kami/SemFacts.v b/Kami/SemFacts.v
index 13463b19..a4e04054 100644
--- a/Kami/SemFacts.v
+++ b/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.
 
diff --git a/Kami/Semantics.v b/Kami/Semantics.v
index 1fb3fc45..c6cf3050 100644
--- a/Kami/Semantics.v
+++ b/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.
diff --git a/Kami/Specialize.v b/Kami/Specialize.v
index bc939237..6131bf25 100644
--- a/Kami/Specialize.v
+++ b/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.
 
diff --git a/Kami/StepDet.v b/Kami/StepDet.v
index 6218ca31..4d6ac1ca 100644
--- a/Kami/StepDet.v
+++ b/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) :=
diff --git a/Kami/Substitute.v b/Kami/Substitute.v
index bca265ee..d99924c2 100644
--- a/Kami/Substitute.v
+++ b/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).
diff --git a/Kami/Syntax.v b/Kami/Syntax.v
index 5d4e6929..cf627fb7 100644
--- a/Kami/Syntax.v
+++ b/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` *)
diff --git a/Kami/Synthesize.v b/Kami/Synthesize.v
index 3f4b0815..eeae0f4f 100644
--- a/Kami/Synthesize.v
+++ b/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.
 
diff --git a/Kami/Tactics.v b/Kami/Tactics.v
index 43276d17..4dec7299 100644
--- a/Kami/Tactics.v
+++ b/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
diff --git a/Kami/Tutorial.v b/Kami/Tutorial.v
index c56207a4..8e7fd4f0 100644
--- a/Kami/Tutorial.v
+++ b/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. *)
 
diff --git a/Kami/Wf.v b/Kami/Wf.v
index da5571af..711714f6 100644
--- a/Kami/Wf.v
+++ b/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.