Skip to content

Commit

Permalink
Correct improper CS declaration
Browse files Browse the repository at this point in the history
Type cast on head constant spoils projection registration (Coq misfeature).
  • Loading branch information
Georges Gonthier committed Dec 4, 2015
1 parent a2b30aa commit 903a5e4
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion mathcomp/field/fieldext.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 903a5e4

Please sign in to comment.