Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

subfilter doesn't exists #84

Closed
hivert opened this issue Nov 18, 2016 · 4 comments
Closed

subfilter doesn't exists #84

hivert opened this issue Nov 18, 2016 · 4 comments
Assignees
Labels
kind: enhancement Issue or PR about addition of features.
Milestone

Comments

@hivert
Copy link
Member

hivert commented Nov 18, 2016

The documentation at the beggining of seq.v speak about a subfilter function:

(* 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.                                 *)

I can't find anything like that in the file. Should we simply remove it from the documentation ?

Meta question: Should I ask this here or on the mailing list ?

@gares gares added the kind: enhancement Issue or PR about addition of features. label Jan 19, 2017
@gares
Copy link
Member

gares commented Jan 19, 2017

linked to issue #89

@gares gares added this to the 1.7 milestone Jan 19, 2017
@amahboubi
Copy link
Member

Hello @hivert ! This issue has been open for long now... Is it ok if we just merge PR #106 ? Or is there some more documentation needed about how to do that now?

@hivert
Copy link
Member Author

hivert commented Mar 9, 2017

Hello @amahboubi ! I'm not sure to understand your question. Are you asking whether you should suggest the user to uses something like pmap insub (That's the correct way isn't it) ? If so, I thing simply removing the doc as in #106 is Ok.

@CohenCyril
Copy link
Member

I agree too, it is done.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Issue or PR about addition of features.
Projects
None yet
Development

No branches or pull requests

4 participants