diff --git a/theories/AAC.v b/theories/AAC.v
index adf74a2..287de83 100644
--- a/theories/AAC.v
+++ b/theories/AAC.v
@@ -34,6 +34,7 @@ From AAC_tactics Require Import Utils Constants.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope signature_scope.
 
diff --git a/theories/Utils.v b/theories/Utils.v
index 0e4a936..1bd51ca 100644
--- a/theories/Utils.v
+++ b/theories/Utils.v
@@ -12,6 +12,7 @@ From Stdlib Require Import Arith NArith List RelationClasses.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
+#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** ** Utilities for positive numbers