From 00f593f9361af73290443fce9b16cc0cbe9884f4 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Thu, 26 Sep 2019 22:59:01 +0200
Subject: Non-distributive lattice

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

(limited to 'mathcomp/algebra/ssrint.v')

diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index dd72017..3903609 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -431,6 +431,7 @@ End intOrdered.
 End intOrdered.
 
 Canonical int_porderType := POrderType ring_display int intOrdered.Mixin.
+Canonical int_latticeType := LatticeType int intOrdered.Mixin.
 Canonical int_distrLatticeType := DistrLatticeType int intOrdered.Mixin.
 Canonical int_orderType := OrderType int intOrdered.lez_total.
 Canonical int_numDomainType := NumDomainType int intOrdered.Mixin.
-- 
cgit v1.2.3