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

---
 src/Util/GlobalSettings.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Util/GlobalSettings.v b/src/Util/GlobalSettings.v
index f54b106526..a01c2db200 100644
--- a/src/Util/GlobalSettings.v
+++ b/src/Util/GlobalSettings.v
@@ -4,6 +4,7 @@
     ex_intro x y => _ end], rather than [match p with ex_intro _ x y
     => _ end]. *)
 Global Set Asymmetric Patterns.
+#[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.
 
 (** Enforce uniform parameters *)
 Global Set Uniform Inductive Parameters.