From ab387ba789820bc9115db5e0ae6ac29be7983e5b Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 22 Jul 2015 13:48:23 +0200
Subject: forgotten import

---
 mathcomp/algebra/ring_quotient.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v
index c1427f3..bcd3b85 100644
--- a/mathcomp/algebra/ring_quotient.v
+++ b/mathcomp/algebra/ring_quotient.v
@@ -1,4 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp
 Require Import eqtype choice ssreflect ssrbool ssrnat ssrfun seq.
 From mathcomp
-- 
cgit v1.2.3