From c67dde4080b9c4470b8ab4ff828707fb0044d3dc Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Tue, 21 Apr 2020 01:52:32 +0900
Subject: Add dual_finLatticeType and fix dual_finDistrLatticeType

This fixes two issues:
- dual_finLatticeType was missing, and
- dual_finDistrLatticeType was just an identity function.
---
 mathcomp/ssreflect/order.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 38ee13d..90ddfcb 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -3549,6 +3549,10 @@ Lemma botEdual : (dual_bottom : L^d) = 1 :> L. Proof. by []. Qed.
 Lemma topEdual : (dual_top : L^d) = 0 :> L. Proof. by []. Qed.
 
 End DualTBLattice.
+
+Canonical dual_finLatticeType d (T : finLatticeType d) :=
+  [finLatticeType of T^d].
+
 End DualTBLattice.
 
 Module Import TBLatticeTheory.
@@ -3682,11 +3686,12 @@ Context {L : tbDistrLatticeType}.
 Canonical dual_bDistrLatticeType := [bDistrLatticeType of L^d].
 Canonical dual_tbDistrLatticeType := [tbDistrLatticeType of L^d].
 
+End DualTBDistrLattice.
+
 Canonical dual_finDistrLatticeType d (T : finDistrLatticeType d) :=
   [finDistrLatticeType of T^d].
 
 End DualTBDistrLattice.
-End DualTBDistrLattice.
 
 Module Import TBDistrLatticeTheory.
 Section TBDistrLatticeTheory.
-- 
cgit v1.2.3