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/seq.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

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

diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 4e4c77b..9c13df3 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1309,14 +1309,14 @@ Definition inE := (mem_seq1, in_cons, inE).
 
 Prenex Implicits mem_seq1 uniq undup index.
 
-Arguments eqseqP [T x y].
-Arguments hasP [T a s].
-Arguments hasPn [T a s].
-Arguments allP [T a s].
-Arguments allPn [T a s].
-Arguments nseqP [T n x y].
-Arguments count_memPn [T x s].
-Prenex Implicits eqseqP hasP hasPn allP allPn nseqP count_memPn.
+Arguments eqseq {T} !_ !_.
+Arguments eqseqP {T x y}.
+Arguments hasP {T a s}.
+Arguments hasPn {T a s}.
+Arguments allP {T a s}.
+Arguments allPn {T a s}.
+Arguments nseqP {T n x y}.
+Arguments count_memPn {T x s}.
 
 Section NthTheory.
 
-- 
cgit v1.2.3