From 181597904ae9211facaa406371b5d54d61f40cbf Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Jul 2019 10:16:26 +0200
Subject: Remove library-specific code for `Import`.

Libraries are now handled like other modules.
---
 plugins/btauto/Algebra.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/btauto')

diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index 638a4cef21..3ad5bc9f2d 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -1,4 +1,4 @@
-Require Import Bool PArith DecidableClass Omega Lia.
+Require Import Bool PArith DecidableClass Ring Omega Lia.
 
 Ltac bool :=
 repeat match goal with
-- 
cgit v1.2.3