From 40a56079d1a7ddd5a24445605a7d7dc1fb5c5b6c Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Fri, 15 Nov 2019 14:28:18 +0100
Subject: fix in ssralg (#421)

* missing exports of lemmas `commrB`, `commr_sum` and  `commr_prod`
* missing `regular_*` canonical exports

---
 mathcomp/algebra/ssralg.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index f385ad5..4b1d85c 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -5653,6 +5653,9 @@ Definition commr1 := commr1.
 Definition commrN := commrN.
 Definition commrN1 := commrN1.
 Definition commrD := commrD.
+Definition commrB := commrB.
+Definition commr_sum := commr_sum.
+Definition commr_prod := commr_prod.
 Definition commrMn := commrMn.
 Definition commrM := commrM.
 Definition commr_nat := commr_nat.
@@ -6152,6 +6155,8 @@ Canonical regular_algType.
 Canonical regular_unitRingType.
 Canonical regular_comUnitRingType.
 Canonical regular_unitAlgType.
+Canonical regular_comAlgType.
+Canonical regular_comUnitAlgType.
 Canonical regular_idomainType.
 Canonical regular_fieldType.
 
-- 
cgit v1.2.3