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

---
 examples/AlmostFull.v        | 1 +
 test-suite/cfold.v           | 1 +
 test-suite/issues/issue212.v | 1 +
 test-suite/issues/issue349.v | 1 +
 test-suite/nestedobls.v      | 3 ++-
 5 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/examples/AlmostFull.v b/examples/AlmostFull.v
index 7c69a924..e5f6cd85 100644
--- a/examples/AlmostFull.v
+++ b/examples/AlmostFull.v
@@ -12,6 +12,7 @@ From Stdlib Require Import FunctionalExtensionality.
 Set Equations Transparent.
 Set Keyed Unification.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 Local Set Firstorder Solver auto with arith core datatypes.
 
 Ltac intuition_solver ::= auto with *.
diff --git a/test-suite/cfold.v b/test-suite/cfold.v
index 6214b311..bcc2f1d9 100644
--- a/test-suite/cfold.v
+++ b/test-suite/cfold.v
@@ -10,6 +10,7 @@ From Stdlib Require Import Bool.Bool.
 Set Keyed Unification.
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Inductive type : Set :=
 | Nat : type
diff --git a/test-suite/issues/issue212.v b/test-suite/issues/issue212.v
index c43c0900..d0b81ed7 100644
--- a/test-suite/issues/issue212.v
+++ b/test-suite/issues/issue212.v
@@ -3,6 +3,7 @@ From Stdlib Require Import Lia ssreflect.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Import ListNotations.
 
diff --git a/test-suite/issues/issue349.v b/test-suite/issues/issue349.v
index 15b97124..158c6700 100644
--- a/test-suite/issues/issue349.v
+++ b/test-suite/issues/issue349.v
@@ -1,4 +1,5 @@
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 Set Implicit Arguments.
 
 From Stdlib Require Import Lia Lists.List.
diff --git a/test-suite/nestedobls.v b/test-suite/nestedobls.v
index 38abd3a4..64780f02 100644
--- a/test-suite/nestedobls.v
+++ b/test-suite/nestedobls.v
@@ -7,6 +7,7 @@
 (**********************************************************************)
 
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 Set Implicit Arguments.
 Unset Strict Implicit.
 From Stdlib Require Import Arith.
@@ -39,4 +40,4 @@ Module Bug.
                       | exist _ k p'' := exist _ k _ } } }.
   Proof. all:(clear test'; unfold MR; simpl; auto with arith). lia. Defined.
 
-End Bug.
\ No newline at end of file
+End Bug.