diff options
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 2e0d1c1..5ec8ee2 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -86,9 +86,6 @@ Require Import ssrfun ssrbool eqtype ssrnat. (* ** Filtering: *) (* filter p s == the subsequence of s consisting of all the items *) (* for which the (boolean) predicate p holds. *) -(* subfilter s : seq sT == when sT has a subType p structure, the sequence *) -(* of items of type sT corresponding to items of s *) -(* for which p holds. *) (* rem x s == the subsequence of s, where the first occurrence *) (* of x has been removed (compare filter (predC1 x) s *) (* where ALL occurrences of x are removed). *) @@ -859,7 +856,7 @@ Implicit Arguments revK [[T]]. Section EqSeq. Variables (n0 : nat) (T : eqType) (x0 : T). -Notation Local nth := (nth x0). +Local Notation nth := (nth x0). Implicit Type s : seq T. Implicit Types x y z : T. |