Merge pull request #242 from anton-trunov/remove-canonical-for-mixins

Document and review the usage of canonical Equality mixins

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.