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 +-
 plugins/setoid_ring/Cring.v | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

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
diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
index 4f3f0c3878..df0313a624 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -19,6 +19,7 @@ Require Export Algebra_syntax.
 Require Export Ncring.
 Require Export Ncring_initial.
 Require Export Ncring_tac.
+Require Import InitialRing.
 
 Class Cring {R:Type}`{Rr:Ring R} := 
  cring_mul_comm: forall x y:R, x * y == y * x.
-- 
cgit v1.2.3