From 903a5e41e93449fe257e289e75ecb5e948b092fe Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Tue, 1 Dec 2015 07:50:34 +0000
Subject: Correct improper CS declaration

Type cast on head constant spoils projection registration (Coq misfeature).
---
 mathcomp/field/fieldext.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v
index 1e14ab7..6214ef0 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -352,7 +352,8 @@ Proof. by rewrite (sameP FadjoinP andP) sub1v. Qed.
 Fact vsval_multiplicative K : multiplicative (vsval : subvs_of K -> L).
 Proof. by split => //=; apply: algid1. Qed.
 Canonical vsval_rmorphism K := AddRMorphism (vsval_multiplicative K).
-Canonical vsval_lrmorphism K := [lrmorphism of (vsval : subvs_of K -> L)].
+Canonical vsval_lrmorphism K : {lrmorphism subvs_of K -> L} :=
+  [lrmorphism of vsval].
 
 Lemma vsval_invf K (w : subvs_of K) : val w^-1 = (vsval w)^-1.
 Proof.
-- 
cgit v1.2.3