From 3c20f9049d4881a9f16404929e5d135b9ef23ee6 Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Tue, 7 Feb 2017 20:52:50 +0900
Subject: remove documentation for subfilter.

subfilter was exist at ssreflect-1.1 and removed at ssreflect-1.2.
---
 mathcomp/ssreflect/seq.v | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'mathcomp')

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).           *)
-- 
cgit v1.2.3