diff --git a/src/Compilers/MultiSizeTest.v b/src/Compilers/MultiSizeTest.v
index 2ce932e8e6..4c5acff287 100644
--- a/src/Compilers/MultiSizeTest.v
+++ b/src/Compilers/MultiSizeTest.v
@@ -4,6 +4,7 @@ Require Import Crypto.Compilers.SmartMap.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** * Preliminaries: bounded and unbounded number types *)
 
diff --git a/src/Util/GlobalSettings.v b/src/Util/GlobalSettings.v
index 9c4be3ad8d..950de131be 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.