From b5f1fecda45943ef81cb84dee85b5eda27234e65 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Tue, 5 Mar 2019 17:08:36 +0100
Subject: Export addrKA and subrKA from GRing.Theory

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

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 47cee1f..a3b4545 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -5380,6 +5380,8 @@ Definition oppr0 := oppr0.
 Definition oppr_eq0 := oppr_eq0.
 Definition opprD := opprD.
 Definition opprB := opprB.
+Definition addrKA := addrKA.
+Definition subrKA := subrKA.
 Definition subr0 := subr0.
 Definition sub0r := sub0r.
 Definition subr_eq := subr_eq.
-- 
cgit v1.2.3