diff --git a/Kami/Decomposition.v b/Kami/Decomposition.v
index 4871fc2..ef9cb75 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 0cde3f7..3a75ccb 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 3d49fca..da2c316 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 48a55e8..739b8d2 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 13c2362..fcd0724 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 e0a6048..0fb3689 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 458cd99..d195bc8 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 9b85719..1d0e3cd 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 7456464..f619144 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 b56f833..b3215e1 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 2615b66..2db591a 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 c8da272..d3e8962 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 51b3003..d26c971 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 846392c..7e5a315 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 daa0ec6..25a2b44 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 0937455..c193f84 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 694b6cd..af42c21 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 6a4b803..b506243 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 f3d41f6..6dd0974 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 f6b941c..c150e91 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 c803593..b715c0f 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 58073c9..3f4d55e 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 bf86a91..1f350c6 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 225d7a6..e8e1d36 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 79ae6bf..68c7b49 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 822008c..674d732 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 13463b1..a4e0405 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 1fb3fc4..c6cf305 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 bc93923..6131bf2 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 6218ca3..4d6ac1c 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 bca265e..d99924c 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 5d4e692..cf627fb 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 3f4b081..eeae0f4 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 43276d1..4dec729 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 c56207a..8e7fd4f 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 da5571a..711714f 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.