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/ssreflect/tuple.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/tuple.v')

diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 64585f6..38e3dbe 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -360,7 +360,12 @@ Section UseFinTuple.
 
 Variables (n : nat) (T : finType).
 
-Canonical tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T).
+(* tuple_finMixin could, in principle, be made Canonical to allow for folding *)
+(* Finite.enum of a finite tuple type (see comments around eqE in eqtype.v),  *)
+(* but in practice it will not work because the mixin_enum projector          *)
+(* has been burried under an opaque alias, to avoid some performance issues   *)
+(* during type inference.                                                     *)
+Definition tuple_finMixin := Eval hnf in FinMixin (@FinTuple.enumP n T).
 Canonical tuple_finType := Eval hnf in FinType (n.-tuple T) tuple_finMixin.
 Canonical tuple_subFinType := Eval hnf in [subFinType of n.-tuple T].
 
-- 
cgit v1.2.3