From 851d7d2dd8d968a00c2c7043ab4c1a7d5c943389 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Wed, 14 Nov 2018 18:08:19 +0100
Subject: 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.
---
 mathcomp/algebra/vector.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra')

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.
-- 
cgit v1.2.3