diff options
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 16 |
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. |