From 8497827e38547e6a14586fbdf5600fb898efd1da Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Sep 2017 17:51:24 +0200
Subject: [PATCH] Get rid of `Automatic Coercions Import`, it is deprecated.

---
 theories/base.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index c3009cd3..0a0fd53c 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.
-- 
GitLab