diff options
| author | Georges Gonthier | 2015-12-01 07:50:34 +0000 |
|---|---|---|
| committer | Georges Gonthier | 2015-12-04 15:07:17 +0000 |
| commit | 903a5e41e93449fe257e289e75ecb5e948b092fe (patch) | |
| tree | 1ea3fef613708f79e98c7cdcbdf978d1977de1af /mathcomp/field | |
| parent | a2b30aa3fd9e2204dbbffa85c04c7e7b9992b53a (diff) | |
Correct improper CS declaration
Type cast on head constant spoils projection registration (Coq misfeature).
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/fieldext.v | 3 |
1 files changed, 2 insertions, 1 deletions
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. |