diff options
| author | Anton Trunov | 2018-11-14 18:08:19 +0100 |
|---|---|---|
| committer | Anton Trunov | 2018-11-15 11:42:36 +0100 |
| commit | 851d7d2dd8d968a00c2c7043ab4c1a7d5c943389 (patch) | |
| tree | 6659f281601a67038b17fa7a9f96a7be9a63b594 /mathcomp/algebra/vector.v | |
| parent | 8c2b4474a29c6213a79676a1e76a8ce936e6f6d6 (diff) | |
Tweak code related to canonical mixins
Remove some unused canonical mixins.
Change simplification behavior of concrete comparison functions to allow for
better simplification using unfolding and sebsequent folding back e.g. with
`rewrite !eqE /= -!eqE`.
A bit of cleanup for `Prenex Implicits` declarations.
Document some explanations by G. Gonthier.
Diffstat (limited to 'mathcomp/algebra/vector.v')
| -rw-r--r-- | mathcomp/algebra/vector.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index a2346a2..cda2876 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1302,7 +1302,7 @@ Section LfunZmodType. Variables (R : ringType) (aT rT : vectType R). Implicit Types f g h : 'Hom(aT, rT). -Canonical lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:]. +Definition lfun_eqMixin := Eval hnf in [eqMixin of 'Hom(aT, rT) by <:]. Canonical lfun_eqType := EqType 'Hom(aT, rT) lfun_eqMixin. Definition lfun_choiceMixin := [choiceMixin of 'Hom(aT, rT) by <:]. Canonical lfun_choiceType := ChoiceType 'Hom(aT, rT) lfun_choiceMixin. |