From c4a2f8e4f80764266406e7166572e553c0ff2f5f Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Sat, 4 Feb 2017 01:15:26 +0100
Subject: adding rquot_comRingType

---
 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 8d8eaaf..8745049 100644
--- a/mathcomp/algebra/ring_quotient.v
+++ b/mathcomp/algebra/ring_quotient.v
@@ -648,6 +648,7 @@ Canonical Quotient.rquot_eqType.
 Canonical Quotient.rquot_choiceType.
 Canonical Quotient.rquot_zmodType.
 Canonical Quotient.rquot_ringType.
+Canonical Quotient.rquot_comRingType.
 Canonical Quotient.rquot_quotType.
 Canonical Quotient.rquot_eqQuotType.
 Canonical Quotient.rquot_zmodQuotType.
-- 
cgit v1.2.3