diff options
| author | Tanaka Akira | 2017-02-07 20:52:50 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2017-02-07 20:52:50 +0900 |
| commit | 3c20f9049d4881a9f16404929e5d135b9ef23ee6 (patch) | |
| tree | a8c819723ebc99c49114cf936383a32f9cd53613 /mathcomp | |
| parent | 8ec7ab833235c71ac701ad4a4fa09aca87008e4f (diff) | |
remove documentation for subfilter.
subfilter was exist at ssreflect-1.1 and removed at ssreflect-1.2.
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index b622543..32f507d 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). *) |