diff --git a/theories/Data/Checked.v b/theories/Data/Checked.v
index 1f2606d7..8a0b0384 100644
--- a/theories/Data/Checked.v
+++ b/theories/Data/Checked.v
@@ -1,6 +1,7 @@
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Section checked.
   Context {T : Type}.
@@ -35,4 +36,4 @@ Section checked.
       | Failure => None
     end.
 
-End checked.
\ No newline at end of file
+End checked.
diff --git a/theories/Data/Fin.v b/theories/Data/Fin.v
index 6403776e..b0b8e851 100644
--- a/theories/Data/Fin.v
+++ b/theories/Data/Fin.v
@@ -7,6 +7,7 @@ Require Import ExtLib.Tactics.Injection.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 (** `fin n` corresponds to "naturals less than `n`",
     i.e. a finite set of size n
diff --git a/theories/Data/HList.v b/theories/Data/HList.v
index 67091751..ffc88157 100644
--- a/theories/Data/HList.v
+++ b/theories/Data/HList.v
@@ -11,6 +11,7 @@ Require Import Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 Set Universe Polymorphism.
 Set Polymorphic Inductive Cumulativity.
 Set Printing Universes.
diff --git a/theories/Data/Member.v b/theories/Data/Member.v
index 6a806c35..ba91f991 100644
--- a/theories/Data/Member.v
+++ b/theories/Data/Member.v
@@ -11,6 +11,7 @@ Require Import ExtLib.Tactics.EqDep.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Section member.
   Context {T : Type}.
diff --git a/theories/Data/Tuple.v b/theories/Data/Tuple.v
index 7b079b2c..86fed00f 100644
--- a/theories/Data/Tuple.v
+++ b/theories/Data/Tuple.v
@@ -3,6 +3,7 @@ Require Import ExtLib.Data.Fin.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Fixpoint vector (T : Type) (n : nat) : Type :=
   match n with
diff --git a/theories/Data/Vector.v b/theories/Data/Vector.v
index 6b41f2c4..da176e20 100644
--- a/theories/Data/Vector.v
+++ b/theories/Data/Vector.v
@@ -3,6 +3,7 @@ Require Import ExtLib.Data.Fin.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Inductive vector T : nat -> Type :=
 | Vnil : vector T 0
diff --git a/theories/Programming/With.v b/theories/Programming/With.v
index e5b8f4bd..4aee7238 100644
--- a/theories/Programming/With.v
+++ b/theories/Programming/With.v
@@ -1,6 +1,7 @@
 Require Import Coq.Lists.List.
 
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Fixpoint Ctor {T : Type} (ls : list {x : Type & T -> x}) : Type :=
   match ls with
diff --git a/theories/Relations/TransitiveClosure.v b/theories/Relations/TransitiveClosure.v
index 0f1eafb0..ef642682 100644
--- a/theories/Relations/TransitiveClosure.v
+++ b/theories/Relations/TransitiveClosure.v
@@ -4,6 +4,7 @@ Require Import Coq.Setoids.Setoid.
 Set Implicit Arguments.
 Set Strict Implicit.
 Set Asymmetric Patterns.
+Set Asymmetric Patterns No Implicits.
 
 Section parametric.
   Variable T : Type.