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.

1 files changed, 8 insertions, 8 deletions

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.