diff --git a/theories/base.v b/theories/base.v
index c3009cd38339f6209649e1f7edb131b7e6cbc4f9..0a0fd53cec72355ed1cbc02ba22be5a917e81a28 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -5,7 +5,6 @@ that are used throughout the whole development. Most importantly it contains
 abstract interfaces for ordered structures, collections, and various other data
 structures. *)
 Global Generalizable All Variables.
-Global Set Automatic Coercions Import.
 Global Set Asymmetric Patterns.
 Global Unset Transparent Obligations.
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.