From a2b30aa3fd9e2204dbbffa85c04c7e7b9992b53a Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Mon, 30 Nov 2015 18:29:12 +0000
Subject: Add finLmodType, finLalgType and finAlgType instances

---
 mathcomp/algebra/matrix.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 18790ee..4469266 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -2053,8 +2053,12 @@ Proof.
 by apply/matrixP=> k i; rewrite !mxE; apply: eq_bigr => j _; rewrite !mxE.
 Qed.
 
+Canonical matrix_finLmodType (R : finRingType) m n :=
+  [finLmodType R of 'M[R]_(m, n)].
 Canonical matrix_finRingType (R : finRingType) n' :=
   Eval hnf in [finRingType of 'M[R]_n'.+1].
+Canonical matrix_finLalgType (R : finRingType) n' :=
+  [finLalgType R of 'M[R]_n'.+1].
 
 (* Parametricity over the algebra structure. *)
 Section MapRingMatrix.
@@ -2478,6 +2482,9 @@ Implicit Arguments lin_mul_row [R m n].
 Implicit Arguments lin_mulmx [R m n p].
 Prenex Implicits lin_mul_row lin_mulmx.
 
+Canonical matrix_finAlgType (R : finComRingType) n' :=
+  [finAlgType R of 'M[R]_n'.+1].
+
 (*****************************************************************************)
 (********************** Matrix unit ring and inverse matrices ****************)
 (*****************************************************************************)
-- 
cgit v1.2.3